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, 19 insertions, 22 deletions

diff --git a/kernel/modops.mli b/kernel/modops.mli
index d7cdb59ac..3cb8e47bb 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -20,55 +20,52 @@ open Mod_subst
 
 (* Various operations on modules and module types *)
 
-(* recursively unfold MTBdent module types *)
-val scrape_modtype : env -> module_type_body -> module_type_body
-
 (* make the environment entry out of type *)
-val module_body_of_type : module_type_body -> module_body
-
-val module_body_of_spec : module_specification_body -> module_body 
-
-val module_spec_of_body : module_body -> module_specification_body
+val module_body_of_type : struct_expr_body -> module_body
 
 
 val destr_functor : 
-  module_type_body -> mod_bound_id * module_type_body * module_type_body
+  env -> struct_expr_body -> mod_bound_id * struct_expr_body * struct_expr_body
 
-
-val subst_modtype : substitution -> module_type_body -> module_type_body
+val subst_modtype : substitution -> struct_expr_body -> struct_expr_body
 
 val subst_signature_msid :
   mod_self_id -> module_path -> 
-  module_signature_body -> module_signature_body
+  structure_body -> structure_body
+
+(* Evaluation functions *)
+val eval_struct : env -> struct_expr_body -> struct_expr_body
+
+val type_of_mb : env -> module_body -> struct_expr_body
 
 (* [add_signature mp sign env] assumes that the substitution [msid]
    $\mapsto$ [mp] has already been performed (or is not necessary, like
    when [mp = MPself msid]) *)
 val add_signature : 
-  module_path -> module_signature_body -> env -> env
+  module_path -> structure_body -> env -> env
 
 (* adds a module and its components, but not the constraints *)
 val add_module :
-  module_path -> module_body ->  env -> env
+  module_path -> module_body -> env -> env
 
 val check_modpath_equiv : env -> module_path -> module_path -> unit
 
-val strengthen : env -> module_type_body -> module_path -> module_type_body
+val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body
 
 val error_existing_label : label -> 'a
 
-val error_declaration_not_path : module_expr -> 'a
+val error_declaration_not_path : module_struct_entry -> 'a
 
-val error_application_to_not_path : module_expr -> 'a
+val error_application_to_not_path : module_struct_entry -> 'a
 
-val error_not_a_functor : module_expr -> 'a
+val error_not_a_functor :  module_struct_entry -> 'a
 
 val error_incompatible_modtypes : 
-  module_type_body -> module_type_body -> 'a
+    struct_expr_body -> struct_expr_body -> 'a
 
 val error_not_equal : module_path -> module_path -> 'a
 
-val error_not_match : label -> specification_body -> 'a
+val error_not_match : label -> structure_field_body -> 'a
   
 val error_incompatible_labels : label -> label -> 'a
 
@@ -76,7 +73,7 @@ val error_no_such_label : label -> 'a
 
 val error_result_must_be_signature : unit -> 'a
 
-val error_signature_expected : module_type_body -> 'a
+val error_signature_expected : struct_expr_body -> 'a
 
 val error_no_module_to_end : unit -> 'a 
 
@@ -99,4 +96,4 @@ val error_local_context : label option -> 'a
 val error_no_such_label_sub : label->string->string->'a
 
 val resolver_of_environment :
- mod_bound_id -> module_type_body -> module_path -> env -> resolver
+  mod_bound_id -> struct_expr_body -> module_path -> env -> resolver