Add Compl/stdlib for commonly imported stuff from Coq stdlib.
Mv {nat,ord}_compl, Finite_{family,table} from Algebra to Compl. Smooth imports.
Showing
- FEM/Algebra/AffineSpace.v 3 additions, 2 deletionsFEM/Algebra/AffineSpace.v
- FEM/Algebra/Algebra.v 0 additions, 1 deletionFEM/Algebra/Algebra.v
- FEM/Algebra/Finite_dim.v 3 additions, 2 deletionsFEM/Algebra/Finite_dim.v
- FEM/Algebra/Finite_dim_R.v 3 additions, 2 deletionsFEM/Algebra/Finite_dim_R.v
- FEM/Algebra/Group_compl.v 3 additions, 2 deletionsFEM/Algebra/Group_compl.v
- FEM/Algebra/ModuleSpace_R_compl.v 3 additions, 2 deletionsFEM/Algebra/ModuleSpace_R_compl.v
- FEM/Algebra/ModuleSpace_compl.v 3 additions, 2 deletionsFEM/Algebra/ModuleSpace_compl.v
- FEM/Algebra/MonoidComp.v 3 additions, 2 deletionsFEM/Algebra/MonoidComp.v
- FEM/Algebra/MonoidMult.v 3 additions, 1 deletionFEM/Algebra/MonoidMult.v
- FEM/Algebra/Monoid_compl.v 2 additions, 2 deletionsFEM/Algebra/Monoid_compl.v
- FEM/Algebra/Ring_compl.v 2 additions, 3 deletionsFEM/Algebra/Ring_compl.v
- FEM/Algebra/Sub_struct.v 3 additions, 1 deletionFEM/Algebra/Sub_struct.v
- FEM/Algebra/matrix.v 3 additions, 2 deletionsFEM/Algebra/matrix.v
- FEM/Compl/Compl.v 1 addition, 0 deletionsFEM/Compl/Compl.v
- FEM/Compl/Finite_family.v 4 additions, 2 deletionsFEM/Compl/Finite_family.v
- FEM/Compl/Finite_table.v 3 additions, 2 deletionsFEM/Compl/Finite_table.v
- FEM/Compl/Function_compl.v 4 additions, 2 deletionsFEM/Compl/Function_compl.v
- FEM/Compl/Function_sub.v 4 additions, 2 deletionsFEM/Compl/Function_sub.v
- FEM/Compl/Subset_compl.v 4 additions, 2 deletionsFEM/Compl/Subset_compl.v
- FEM/Compl/logic_compl.v 7 additions, 1 deletionFEM/Compl/logic_compl.v
Loading
Please register or sign in to comment