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

2 files changed, 12 insertions, 3 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fed36d004..ec60cc52e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -470,10 +470,17 @@ let vernac_end_modtype id =
   if_verbose message 
     ("Module Type "^ string_of_id id ^" is defined")
 
-
+let vernac_include = function
+  | CIMTE mty_ast ->
+      Declaremods.declare_include Modintern.interp_modtype mty_ast false
+  | CIME mexpr_ast ->
+      Declaremods.declare_include Modintern.interp_modexpr mexpr_ast true
+	  
+	  
+	  
 (**********************)
 (* Gallina extensions *)
-
+	  
 let vernac_record struc binders sort nameopt cfs =
   let const = match nameopt with 
     | None -> add_prefix "Build_" (snd (snd struc))
@@ -1198,7 +1205,8 @@ let interp c = match c with
       vernac_define_module export id bl mtyo mexpro
   | VernacDeclareModuleType ((_,id),bl,mtyo) -> 
       vernac_declare_module_type id bl mtyo
-
+  | VernacInclude (in_ast) ->
+      vernac_include in_ast
   (* Gallina extensions *)
   | VernacBeginSection (_,id) -> vernac_begin_section id
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 3571b121b..cf7fb72c6 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -249,6 +249,7 @@ type vernac_expr =
       module_binder list * (module_type_ast * bool) option * module_ast option
   | VernacDeclareModuleType of lident * 
       module_binder list * module_type_ast option
+  | VernacInclude of include_ast
 
   (* Solving *)