Make {filter0F,filter_n0F,split0F}{,_gen} abbreviations.
Generalize {filter0F,filter_n0F}_correct into filter_{,n}eqF_correct. Rm now useless specific results.
Showing
- Algebra/AffineSpace/AffineSpace_baryc.v 1 addition, 1 deletionAlgebra/AffineSpace/AffineSpace_baryc.v
- Algebra/ModuleSpace/ModuleSpace_lin_comb.v 6 additions, 6 deletionsAlgebra/ModuleSpace/ModuleSpace_lin_comb.v
- Algebra/Monoid/Monoid_FF.v 22 additions, 74 deletionsAlgebra/Monoid/Monoid_FF.v
- Subsets/Finite_family.v 7 additions, 0 deletionsSubsets/Finite_family.v
Loading
Please register or sign in to comment