1 files changed, 40 insertions, 19 deletions

diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index b4a8fdfd..b46cf42d 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -68,12 +68,17 @@ let print_kn locals kn =
 	with
 	    Not_found -> print_modpath locals kn
 
+(** Each time we have to print a non-globally visible structure,
+    we place its elements in a fake fresh namespace. *)
+
+let mk_fake_top =
+  let r = ref 0 in
+  fun () -> incr r; id_of_string ("FAKETOP"^(string_of_int !r))
+
 let nametab_register_dir mp =
-  let id = id_of_string "FAKETOP" in
-  let fp = Libnames.make_path empty_dirpath id in
+  let id = mk_fake_top () in
   let dir = make_dirpath [id] in
-  Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath)));
-  fp
+  Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath)))
 
 (** Nota: the [global_reference] we register in the nametab below
     might differ from internal ones, since we cannot recreate here
@@ -81,9 +86,10 @@ let nametab_register_dir mp =
     the user names. This works nonetheless since we search now
     [Nametab.the_globrevtab] modulo user name. *)
 
-let nametab_register_body mp fp (l,body) =
+let nametab_register_body mp dir (l,body) =
   let push id ref =
-    Nametab.push (Nametab.Until 1) (make_path (dirpath fp) id) ref
+    Nametab.push (Nametab.Until (1+List.length (repr_dirpath dir)))
+      (make_path dir id) ref
   in
   match body with
     | SFBmodule _ -> () (* TODO *)
@@ -99,6 +105,27 @@ let nametab_register_body mp fp (l,body) =
 	    mip.mind_consnames)
 	mib.mind_packets
 
+let nametab_register_module_body mp struc =
+  (* If [mp] is a globally visible module, we simply import it *)
+  try Declaremods.really_import_module mp
+  with Not_found ->
+    (* Otherwise we try to emulate an import by playing with nametab *)
+    nametab_register_dir mp;
+    List.iter (nametab_register_body mp empty_dirpath) struc
+
+let nametab_register_module_param mbid seb =
+  (* For algebraic seb, we use a Declaremods function that converts into mse *)
+  try Declaremods.process_module_seb_binding mbid seb
+  with e when Errors.noncritical e ->
+    (* Otherwise, for expanded structure, we try to play with the nametab *)
+    match seb with
+      | SEBstruct struc ->
+        let mp = MPbound mbid in
+        let dir = make_dirpath [id_of_mbid mbid] in
+        nametab_register_dir mp;
+        List.iter (nametab_register_body mp dir) struc
+      | _ -> ()
+
 let print_body is_impl env mp (l,body) =
   let name = str (string_of_label l) in
   hov 2 (match body with
@@ -126,19 +153,11 @@ let print_body is_impl env mp (l,body) =
       try
 	let env = Option.get env in
 	Printer.pr_mutual_inductive_body env (make_mind mp empty_dirpath l) mib
-      with _ ->
+      with e when Errors.noncritical e ->
 	(if mib.mind_finite then str "Inductive " else str "CoInductive")
 	++ name)
 
 let print_struct is_impl env mp struc =
-  begin
-    (* If [mp] is a globally visible module, we simply import it *)
-    try Declaremods.really_import_module mp
-    with _ ->
-    (* Otherwise we try to emulate an import by playing with nametab *)
-      let fp = nametab_register_dir mp in
-      List.iter (nametab_register_body mp fp) struc
-  end;
   prlist_with_sep spc (print_body is_impl env mp) struc
 
 let rec flatten_app mexpr l = match mexpr with
@@ -156,7 +175,7 @@ let rec print_modtype env mp locals mty =
       let seb1 = Option.default mtb1.typ_expr mtb1.typ_expr_alg in
       let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals
       in
-      (try Declaremods.process_module_seb_binding mbid seb1 with _ -> ());
+      nametab_register_module_param mbid seb1;
       hov 2 (str "Funsig" ++ spc () ++ str "(" ++
 	       pr_id (id_of_mbid mbid) ++ str ":" ++
 	       print_modtype env mp1 locals seb1 ++
@@ -164,6 +183,7 @@ let rec print_modtype env mp locals mty =
   | SEBstruct (sign) ->
       let env' = Option.map
 	(Modops.add_signature mp sign Mod_subst.empty_delta_resolver) env in
+      nametab_register_module_body mp sign;
       hv 2 (str "Sig" ++ spc () ++ print_struct false env' mp sign ++
 	    brk (1,-2) ++ str "End")
   | SEBapply _ ->
@@ -190,13 +210,14 @@ let rec print_modexpr env mp locals mexpr = match mexpr with
 	(Modops.add_module (Modops.module_body_of_type mp' mty)) env in
       let typ = Option.default mty.typ_expr mty.typ_expr_alg in
       let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
-      (try Declaremods.process_module_seb_binding mbid typ with _ -> ());
+      nametab_register_module_param mbid typ;
       hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++
 	     str ":" ++ print_modtype env mp' locals typ ++
       str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr)
   | SEBstruct struc ->
       let env' = Option.map
 	(Modops.add_signature mp struc Mod_subst.empty_delta_resolver) env in
+      nametab_register_module_body mp struc;
       hv 2 (str "Struct" ++ spc () ++ print_struct true env' mp struc ++
 	    brk (1,-2) ++ str "End")
   | SEBapply _ ->
@@ -243,7 +264,7 @@ let print_module with_body mp =
   try
     if !short then raise ShortPrinting;
     print_module' (Some (Global.env ())) mp with_body me ++ fnl ()
-  with _ ->
+  with e when Errors.noncritical e ->
     print_module' None mp with_body me ++ fnl ()
 
 let print_modtype kn =
@@ -254,5 +275,5 @@ let print_modtype kn =
      (try
 	if !short then raise ShortPrinting;
 	print_modtype' (Some (Global.env ())) kn mtb.typ_expr
-      with _ ->
+      with e when Errors.noncritical e ->
 	print_modtype' None kn mtb.typ_expr))