Remove useless nonneg hypotheses (LInt_SFp_{correct,ext,ext_ex}).
Rename LInt_SFp -> LInt_SF, *SFp_* -> *SF_* (when there is no nonneg hypothesis), SF_* -> SFplus_* (when there is a nonneg hypothesis), Lint_SFp_eq_other_list -> Lint_SFp_skip_0.
Showing
- Lebesgue/LInt_p.v 8 additions, 8 deletionsLebesgue/LInt_p.v
- Lebesgue/Mp.v 1 addition, 1 deletionLebesgue/Mp.v
- Lebesgue/bochner_integral/BInt_Bif.v 2 additions, 2 deletionsLebesgue/bochner_integral/BInt_Bif.v
- Lebesgue/bochner_integral/Bi_fun.v 3 additions, 3 deletionsLebesgue/bochner_integral/Bi_fun.v
- Lebesgue/bochner_integral/Bsf_Lsf.v 11 additions, 11 deletionsLebesgue/bochner_integral/Bsf_Lsf.v
- Lebesgue/simple_fun.v 60 additions, 68 deletionsLebesgue/simple_fun.v
Loading
Please register or sign in to comment