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, 3 insertions, 3 deletions

diff --git a/library/nametab.mli b/library/nametab.mli
index 66de6a708..eab86db1d 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -73,7 +73,7 @@ type visibility = Until of int | Exactly of int
 val push : visibility -> section_path -> global_reference -> unit
 val push_syntactic_definition : 
   visibility -> section_path -> kernel_name -> unit
-val push_modtype : visibility -> section_path -> kernel_name -> unit
+val push_modtype : visibility -> section_path -> module_path -> unit
 val push_dir : visibility -> dir_path -> global_dir_reference -> unit
 val push_object : visibility -> section_path -> unit
 val push_tactic : visibility -> section_path -> kernel_name -> unit
@@ -106,7 +106,7 @@ val locate_obj : qualid -> section_path
 val locate_constant : qualid -> constant
 val locate_mind : qualid -> mutual_inductive
 val locate_section : qualid -> dir_path
-val locate_modtype : qualid -> kernel_name
+val locate_modtype : qualid -> module_path
 val locate_syntactic_definition : qualid -> kernel_name
 
 type ltac_constant = kernel_name
@@ -161,7 +161,7 @@ val pr_global_env : Idset.t -> global_reference -> std_ppcmds
    Coq.A.B.x that denotes the same object. *)
 
 val shortest_qualid_of_module : module_path -> qualid
-val shortest_qualid_of_modtype : kernel_name -> qualid
+val shortest_qualid_of_modtype : module_path -> qualid
 
 
 (*