Beaoucoup de changements dans la representation interne des modules.

kernel:

-declaration.ml
   unification des representations pour les modules et modules types.
     (type struct_expr_body)

-mod_typing.ml
   le typage des modules est separe de l'evaluation des modules

-modops.ml
   nouvelle fonction qui pour toutes expressions de structure calcule
   sa forme evaluee.(eval_struct)

-safe_typing.ml
  ajout du support du nouvel operateur Include.(add_include).


library:

-declaremods.ml
   nouveaux objets Include et Module-alias et gestion de la resolution de noms pour
   les alias via la nametab.

parsing:

-g_vernac.ml4:
   nouvelles regles pour le support des Includes et pour l'application des signatures
   fonctorielles.


extraction:
  Adaptation a la nouvelle representation des modules et support de l'operateur with.




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10497 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 21 insertions, 34 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 4a5893de8..63c690d48 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -247,44 +247,31 @@ let subst_mind sub mib =
 (*s Modules: signature component specifications, module types, and
   module declarations *)
 
-type specification_body = 
-  | SPBconst of constant_body
-  | SPBmind of mutual_inductive_body
-  | SPBmodule of module_specification_body
-  | SPBmodtype of module_type_body
-
-and module_signature_body = (label * specification_body) list
-
-and module_type_body = 
-  | MTBident of kernel_name
-  | MTBfunsig of mod_bound_id * module_type_body * module_type_body
-  | MTBsig of mod_self_id * module_signature_body
-
-and module_specification_body = 
-    { msb_modtype : module_type_body;
-      msb_equiv : module_path option; 
-      msb_constraints : constraints }
-
-type structure_elem_body = 
-  | SEBconst of constant_body
-  | SEBmind of mutual_inductive_body
-  | SEBmodule of module_body
-  | SEBmodtype of module_type_body
-
-and module_structure_body = (label * structure_elem_body) list
-
-and module_expr_body =
-  | MEBident of module_path
-  | MEBfunctor of mod_bound_id * module_type_body * module_expr_body 
-  | MEBstruct of mod_self_id * module_structure_body
-  | MEBapply of module_expr_body * module_expr_body
+type structure_field_body = 
+  | SFBconst of constant_body
+  | SFBmind of mutual_inductive_body
+  | SFBmodule of module_body
+  | SFBmodtype of struct_expr_body
+
+and structure_body = (label * structure_field_body) list
+
+and struct_expr_body =
+  | SEBident of module_path
+  | SEBfunctor of mod_bound_id * struct_expr_body * struct_expr_body 
+  | SEBstruct of mod_self_id * structure_body
+  | SEBapply of struct_expr_body * struct_expr_body
       * constraints
+  | SEBwith of struct_expr_body * with_declaration_body
 
+and with_declaration_body =
+    With_module_body of identifier list * module_path * constraints
+  | With_definition_body of  identifier list * constant_body
+        
 and module_body = 
-    { mod_expr : module_expr_body option;
-      mod_user_type : module_type_body option;
-      mod_type : module_type_body;
+    { mod_expr : struct_expr_body option;
+      mod_type : struct_expr_body option;
       mod_equiv : module_path option;
       mod_constraints : constraints;
       mod_retroknowledge : Retroknowledge.action list}
 
+type module_type_body = struct_expr_body * module_path option