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, 6 insertions, 5 deletions

diff --git a/library/global.mli b/library/global.mli
index 8633dba76..71617f5a1 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -50,7 +50,7 @@ val add_mind        :
   dir_path -> identifier -> mutual_inductive_entry -> kernel_name
 
 val add_module      : identifier -> module_entry -> module_path
-val add_modtype     : identifier -> module_type_entry -> kernel_name
+val add_modtype     : identifier -> module_struct_entry -> module_path
 
 val add_constraints : constraints -> unit
 
@@ -64,13 +64,14 @@ val set_engagement : engagement -> unit
    of the started module / module type *)
 
 val start_module : identifier -> module_path
-val end_module : identifier -> module_type_entry option -> module_path
+val end_module : identifier -> module_struct_entry option -> module_path
 
-val add_module_parameter : mod_bound_id -> module_type_entry -> unit
+val add_module_parameter : mod_bound_id -> module_struct_entry -> unit
 
 val start_modtype : identifier -> module_path
-val end_modtype : identifier -> kernel_name
+val end_modtype : identifier -> module_path
 
+val add_include : module_struct_entry -> unit
 
 (* Queries *)
 val lookup_named     : variable -> named_declaration
@@ -78,7 +79,7 @@ val lookup_constant  : constant -> constant_body
 val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body
 val lookup_mind      : mutual_inductive -> mutual_inductive_body
 val lookup_module    : module_path -> module_body
-val lookup_modtype   : kernel_name -> module_type_body
+val lookup_modtype   : module_path -> module_type_body
 
 (* Compiled modules *)
 val start_library : dir_path -> module_path