Renommages a faire.

FEM/FE.v

@@ -163,7 +163,7 @@ End is_unisolvent_Fact.
 
 Section FE_Local_simplex.
 
-Inductive geom_family :=  Simplex  | Quad.
+Inductive (*shape_type*)geom_family :=  Simplex  | Quad.
 
 (* TODO: add an admissibility property for the geometrical element?
   Il manque peut-être des hypothèses géométriques 
@@ -177,7 +177,7 @@ Record FE : Type := mk_FE {
   ndof : nat ; (* nb of degrees of freedom - eg number of nodes for Lagrange. *)
   d_pos :    (0 < d)%coq_nat ;
   ndof_pos : (0 < ndof)%coq_nat ;
-  g_family : geom_family ;
+  (*shape*)g_family : geom_family ;
   nvtx : nat := match g_family with (* number of vertices *)
        | Simplex => (S d)
        | Quad => 2^d
@@ -185,10 +185,10 @@ Record FE : Type := mk_FE {
   vtx : '('R^d)^nvtx ; (* vertices of geometrical element *)
   K_geom : 'R^d -> Prop := convex_envelop vtx ; (* geometrical element *)
   P_approx : FRd d -> Prop ; (* Subspace of F *)
-  P_compat_fin : has_dim P_approx ndof ;
-  sigma : '(FRd d -> R)^ndof ;
-  is_linear_mapping_sigma : forall i, is_linear_mapping (sigma i) ;
-  FE_is_unisolvent : is_unisolvent d ndof P_approx P_compat_fin (gather sigma) ;
+  (*P_approx_has_dim *)P_compat_fin : has_dim P_approx ndof ;
+  (*Sigma*)sigma : '(FRd d -> R)^ndof ;
+  (*Sigma_lin_map*)is_linear_mapping_sigma : forall i, is_linear_mapping (sigma i) ;
+  (* unisolvence *)FE_is_unisolvent : is_unisolvent d ndof P_approx P_compat_fin (gather sigma) ;
 }.
 
 Variable fe: FE.