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

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 6fe4d80d4..6712af8b9 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -39,7 +39,7 @@ type object_pr = {
   print_section_variable    : variable -> std_ppcmds;
   print_syntactic_def       : kernel_name -> std_ppcmds;
   print_module              : bool -> Names.module_path -> std_ppcmds;
-  print_modtype             : kernel_name -> std_ppcmds;
+  print_modtype             : module_path -> std_ppcmds;
   print_named_decl          : identifier * constr option * types -> std_ppcmds;
   print_leaf_entry          : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds;
   print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
@@ -175,7 +175,7 @@ type logical_name =
   | Term of global_reference
   | Dir of global_dir_reference
   | Syntactic of kernel_name
-  | ModuleType of qualid * kernel_name
+  | ModuleType of qualid * module_path
   | Undefined of qualid
 
 let locate_any_name ref =
@@ -421,7 +421,8 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
 	  let (mp,_,l) = repr_kn kn in 
 	    Some (print_module with_values (MPdot (mp,l)))
       | (_,"MODULE TYPE") ->
-	  Some (print_modtype kn)
+	  let (mp,_,l) = repr_kn kn in 
+	  Some (print_modtype (MPdot (mp,l)))
       | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
 	    "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None
       (* To deal with forgotten cases... *)
@@ -560,7 +561,9 @@ let print_full_pure_context () =
 	  print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
       | "MODULE TYPE" ->
 	  (* TODO: make it reparsable *)
-	  print_modtype kn ++ str "." ++ fnl () ++ fnl ()
+	  (* TODO: make it reparsable *)
+	  let (mp,_,l) = repr_kn kn in
+	  print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
       | _ -> mt () in
       prec rest ++ pp
   | _::rest -> prec rest