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

diff --git a/library/nametab.ml b/library/nametab.ml
index 9aab07cac..536c9605a 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -263,9 +263,11 @@ type ccitab = extended_global_reference SpTab.t
 let the_ccitab = ref (SpTab.empty : ccitab)
 
 type kntab = kernel_name SpTab.t
-let the_modtypetab = ref (SpTab.empty : kntab)
 let the_tactictab = ref (SpTab.empty : kntab)
 
+type mptab = module_path SpTab.t
+let the_modtypetab = ref (SpTab.empty : mptab)
+
 type objtab = unit SpTab.t
 let the_objtab = ref (SpTab.empty : objtab)
 
@@ -299,8 +301,10 @@ let the_globrevtab = ref (Globrevtab.empty : globrevtab)
 type mprevtab = dir_path MPmap.t
 let the_modrevtab = ref (MPmap.empty : mprevtab)
 
+type mptrevtab = section_path MPmap.t
+let the_modtyperevtab = ref (MPmap.empty : mptrevtab)
+
 type knrevtab = section_path KNmap.t
-let the_modtyperevtab = ref (KNmap.empty : knrevtab)
 let the_tacticrevtab = ref (KNmap.empty : knrevtab)
 
 
@@ -328,7 +332,7 @@ let push = push_cci
 
 let push_modtype vis sp kn = 
   the_modtypetab := SpTab.push vis sp kn !the_modtypetab;
-  the_modtyperevtab := KNmap.add kn sp !the_modtyperevtab
+  the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab
 
 (* This is for tactic definition names *)
 
@@ -483,7 +487,7 @@ let shortest_qualid_of_module mp =
     DirTab.shortest_qualid Idset.empty dir !the_dirtab
 
 let shortest_qualid_of_modtype kn =
-  let sp = KNmap.find kn !the_modtyperevtab in
+  let sp = MPmap.find kn !the_modtyperevtab in
     SpTab.shortest_qualid Idset.empty sp !the_modtypetab
 
 let shortest_qualid_of_tactic kn =
@@ -504,6 +508,7 @@ let inductive_of_reference r =
       user_err_loc (loc_of_reference r,"global_inductive",
         pr_reference r ++ spc () ++ str "is not an inductive type")
 
+
 (********************************************************************)
 
 (********************************************************************)
@@ -520,10 +525,11 @@ let init () =
   the_tactictab := SpTab.empty;
   the_globrevtab := Globrevtab.empty;
   the_modrevtab := MPmap.empty;
-  the_modtyperevtab := KNmap.empty;
+  the_modtyperevtab := MPmap.empty;
   the_tacticrevtab := KNmap.empty
 
 
+
 let freeze () =
   !the_ccitab, 
   !the_dirtab,