WIP: Coq-8.16 compatibility + pre-merge with master branch.
It is not fully compiling yet!
Showing
- Lebesgue/LF_subcover.v 4 additions, 12 deletionsLebesgue/LF_subcover.v
- Lebesgue/LInt_p.v 70 additions, 31 deletionsLebesgue/LInt_p.v
- Lebesgue/Makefile 75 additions, 46 deletionsLebesgue/Makefile
- Lebesgue/Mp.v 33 additions, 12 deletionsLebesgue/Mp.v
- Lebesgue/R_compl.v 18 additions, 21 deletionsLebesgue/R_compl.v
- Lebesgue/Rbar_compl.v 8 additions, 8 deletionsLebesgue/Rbar_compl.v
- Lebesgue/Set_theory/FinBij.v 2 additions, 2 deletionsLebesgue/Set_theory/FinBij.v
- Lebesgue/Set_theory/Set_finite.v 5 additions, 4 deletionsLebesgue/Set_theory/Set_finite.v
- Lebesgue/Set_theory/Set_seq.v 3 additions, 3 deletionsLebesgue/Set_theory/Set_seq.v
- Lebesgue/Set_theory/Set_system/Topology.v 1 addition, 1 deletionLebesgue/Set_theory/Set_system/Topology.v
- Lebesgue/Subset_R.v 6 additions, 0 deletionsLebesgue/Subset_R.v
- Lebesgue/Subset_Rbar.v 7 additions, 0 deletionsLebesgue/Subset_Rbar.v
- Lebesgue/Tonelli.v 66 additions, 44 deletionsLebesgue/Tonelli.v
- Lebesgue/UniformSpace_compl.v 7 additions, 4 deletionsLebesgue/UniformSpace_compl.v
- Lebesgue/_CoqProject 1 addition, 1 deletionLebesgue/_CoqProject
- Lebesgue/bochner_integral/simpl_fun.v 44 additions, 45 deletionsLebesgue/bochner_integral/simpl_fun.v
- Lebesgue/bochner_integral/square_bij.v 2 additions, 2 deletionsLebesgue/bochner_integral/square_bij.v
- Lebesgue/bochner_integral/topology_compl.v 5 additions, 2 deletionsLebesgue/bochner_integral/topology_compl.v
- Lebesgue/countable_sets.v 89 additions, 178 deletionsLebesgue/countable_sets.v
- Lebesgue/list_compl.v 2 additions, 2 deletionsLebesgue/list_compl.v
Loading
Please register or sign in to comment