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

4 files changed, 39 insertions, 20 deletions

diff --git a/interp/modintern.ml b/interp/modintern.ml
index f077bea93..68978080b 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -64,7 +64,6 @@ let lookup_qualid (modtype:bool) qid =
    If found, returns the module_path/kernel_name created from the dirpath
    and the basename. Searches Nametab otherwise.
 *)
-
 let lookup_module (loc,qid) =
   try
     Nametab.locate_module qid
@@ -84,20 +83,23 @@ let transl_with_decl env = function
   | CWith_Definition ((_,fqid),c) ->
       With_Definition (fqid,interp_constr Evd.empty env c)
 
-let rec interp_modtype env = function 
-  | CMTEident qid ->
-      MTEident (lookup_modtype qid)
-  | CMTEwith (mty,decl) ->
-      let mty = interp_modtype env mty in
-      let decl = transl_with_decl env decl in
-	MTEwith(mty,decl)
- 
-
 let rec interp_modexpr env = function 
   | CMEident qid ->
-      MEident (lookup_module qid)
+      MSEident (lookup_module qid)
   | CMEapply (me1,me2) ->
       let me1 = interp_modexpr env me1 in
       let me2 = interp_modexpr env me2 in
-	MEapply(me1,me2)
+	MSEapply(me1,me2)
+
+let rec interp_modtype env = function 
+  | CMTEident qid ->
+      MSEident (lookup_modtype qid)
+  | CMTEapply (mty1,me) -> 
+      let mty' = interp_modtype env mty1 in
+      let me' = interp_modexpr env me in
+	MSEapply(mty',me')
+  | CMTEwith (mty,decl) ->
+      let mty = interp_modtype env mty in
+      let decl = transl_with_decl env decl in
+	MSEwith(mty,decl)
 
diff --git a/interp/modintern.mli b/interp/modintern.mli
index a8676c793..1f27e3c18 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -12,13 +12,17 @@
 open Declarations
 open Environ
 open Entries
+open Util
+open Libnames
+open Names
 open Topconstr
 (*i*)
 
 (* Module expressions and module types are interpreted relatively to 
    eventual functor or funsig arguments. *)
 
-val interp_modtype : env -> module_type_ast -> module_type_entry
+val interp_modtype : env -> module_type_ast -> module_struct_entry
 
-val interp_modexpr : env -> module_ast -> module_expr
+val interp_modexpr : env -> module_ast -> module_struct_entry
 
+val lookup_module : qualid located -> module_path
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index accccdeee..c9a33c7eb 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -887,10 +887,16 @@ type with_declaration_ast =
   | CWith_Module of identifier list located * qualid located
   | CWith_Definition of identifier list located * constr_expr
 
-type module_type_ast = 
-  | CMTEident of qualid located
-  | CMTEwith of module_type_ast * with_declaration_ast
 
 type module_ast = 
   | CMEident of qualid located
   | CMEapply of module_ast * module_ast
+
+type module_type_ast = 
+  | CMTEident of qualid located
+  | CMTEapply of module_type_ast * module_ast
+  | CMTEwith of module_type_ast * with_declaration_ast
+
+type include_ast =
+  | CIMTE of module_type_ast
+  | CIME of module_ast
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 6bfbcf07f..26805aa13 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -224,10 +224,17 @@ type with_declaration_ast =
   | CWith_Module of identifier list located * qualid located
   | CWith_Definition of identifier list located * constr_expr
 
-type module_type_ast = 
-  | CMTEident of qualid located
-  | CMTEwith of module_type_ast * with_declaration_ast
 
 type module_ast = 
   | CMEident of qualid located
   | CMEapply of module_ast * module_ast
+
+type module_type_ast = 
+  | CMTEident of qualid located
+  | CMTEapply of module_type_ast * module_ast
+  | CMTEwith of module_type_ast * with_declaration_ast
+
+type include_ast =
+  | CIMTE of module_type_ast
+  | CIME of module_ast
+