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

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 4f2498dc35..2b41e5a363 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -26,7 +26,7 @@ type globals = {
   env_constants : constant_key Cmap.t;
   env_inductives : mutual_inductive_body KNmap.t;
   env_modules : module_body MPmap.t;
-  env_modtypes : module_type_body KNmap.t }
+  env_modtypes : module_type_body MPmap.t }
 
 type stratification = {
   env_universes : universes;
@@ -60,7 +60,7 @@ let empty_env = {
     env_constants = Cmap.empty;
     env_inductives = KNmap.empty;
     env_modules = MPmap.empty;
-    env_modtypes = KNmap.empty };
+    env_modtypes = MPmap.empty };
   env_named_context = empty_named_context;
   env_named_vals = [];
   env_rel_context = empty_rel_context;