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, 9 insertions, 15 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 17da967c2..89e444a74 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -74,28 +74,22 @@ type specification_entry =
     SPEconst of constant_entry
   | SPEmind of mutual_inductive_entry
   | SPEmodule of module_entry
-  | SPEmodtype of module_type_entry
+  | SPEmodtype of module_struct_entry
 
-and module_type_entry = 
-    MTEident of kernel_name
-  | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry
-  | MTEwith of module_type_entry * with_declaration
-
-and module_signature_entry = (label * specification_entry) list
+and module_struct_entry = 
+    MSEident of module_path
+  | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry
+  | MSEwith of module_struct_entry * with_declaration
+  | MSEapply of module_struct_entry * module_struct_entry
 
 and with_declaration = 
     With_Module of identifier list * module_path
   | With_Definition of identifier list * constr
 
-and module_expr = 
-    MEident of module_path
-  | MEfunctor of mod_bound_id * module_type_entry * module_expr
-  | MEapply of module_expr * module_expr
-
 and module_structure = (label * specification_entry) list
 
-
 and module_entry = 
-    { mod_entry_type : module_type_entry option;
-      mod_entry_expr : module_expr option}
+    { mod_entry_type : module_struct_entry option;
+      mod_entry_expr : module_struct_entry option}
+