Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg

10 files changed, 126 insertions, 34 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 1888ef17..214a6b98 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -146,7 +146,7 @@ let possibly_empty_subentries loc (prods,act) =
     (* an exception rather than returning a value; *)
     (* declares loc because some code can refer to it; *)
     (* ensures loc is used to avoid "unused variable" warning *)
-    (true, <:expr< try Some $aux prods$ with [ _ -> None ] >>)
+    (true, <:expr< try Some $aux prods$ with [ e when Errors.noncritical e -> None ] >>)
   else
     (* Static optimisation *)
     (false, aux prods)
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index c68ba137..12359776 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -365,4 +365,4 @@ let _ =
 let with_grammar_rule_protection f x =
   let fs = freeze () in
   try let a = f x in unfreeze fs; a
-  with e -> unfreeze fs; raise e
+  with reraise -> unfreeze fs; raise reraise
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index d265729a..1609e541 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -126,7 +126,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
 let induction_arg_of_constr (c,lbind as clbind) =
   if lbind = NoBindings then
     try ElimOnIdent (constr_loc c,snd(coerce_to_id c))
-    with _ -> ElimOnConstr clbind
+    with e when Errors.noncritical e -> ElimOnConstr clbind
   else ElimOnConstr clbind
 
 let mkTacCase with_evar = function
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 9dd0e369..869674f4 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -104,7 +104,8 @@ let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
 
 let get_xml_inductive_kn al =
   inductive_of_cdata (* uriType apparent synonym of uri *)
-    (try get_xml_attr "uri" al with _ -> get_xml_attr "uriType" al)
+    (try get_xml_attr "uri" al
+     with e when Errors.noncritical e -> get_xml_attr "uriType" al)
 
 let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al)
 
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index d3eb40d0..99e10908 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -273,7 +273,9 @@ let print_inductive_implicit_args =
 
 let print_inductive_renames =
   print_args_data_of_inductive_ids
-    (fun r -> try List.hd (Arguments_renaming.arguments_names r) with _ -> [])
+    (fun r ->
+      try List.hd (Arguments_renaming.arguments_names r)
+      with e when Errors.noncritical e -> [])
     ((<>) Anonymous)
     print_renames_list
 
@@ -737,7 +739,7 @@ let print_coercions () =
 let index_of_class cl =
   try
     fst (class_info cl)
-  with _ ->
+  with e when Errors.noncritical e ->
     errorlabstrm "index_of_class"
       (pr_class cl ++ spc() ++ str "not a defined class.")
 
@@ -747,7 +749,7 @@ let print_path_between cls clt =
   let p =
     try
       lookup_path_between_class (i,j)
-    with _ ->
+    with e when Errors.noncritical e ->
       errorlabstrm "index_cl_of_id"
         (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
 	 ++ str ".")
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 9f0cb00d..29ebe4fa 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -24,6 +24,7 @@ open Pfedit
 open Ppconstr
 open Constrextern
 open Tacexpr
+open Declarations
 
 open Store.Field
 
@@ -118,6 +119,63 @@ let pr_sort s = pr_glob_sort (extern_sort s)
 
 let _ = Termops.set_print_constr pr_lconstr_env
 
+
+(** Term printers resilient to [Nametab] errors *)
+
+(** When the nametab isn't up-to-date, the term printers above
+    could raise [Not_found] during [Nametab.shortest_qualid_of_global].
+    In this case, we build here a fully-qualified name based upon
+    the kernel modpath and label of constants, and the idents in
+    the [mutual_inductive_body] for the inductives and constructors
+    (needs an environment for this). *)
+
+let id_of_global env = function
+  | ConstRef kn -> id_of_label (con_label kn)
+  | IndRef (kn,0) -> id_of_label (mind_label kn)
+  | IndRef (kn,i) ->
+    (Environ.lookup_mind kn env).mind_packets.(i).mind_typename
+  | ConstructRef ((kn,i),j) ->
+    (Environ.lookup_mind kn env).mind_packets.(i).mind_consnames.(j-1)
+  | VarRef v -> v
+
+let cons_dirpath id dp = make_dirpath (id :: repr_dirpath dp)
+
+let rec dirpath_of_mp = function
+  | MPfile sl -> sl
+  | MPbound uid -> make_dirpath [id_of_mbid uid]
+  | MPdot (mp,l) -> cons_dirpath (id_of_label l) (dirpath_of_mp mp)
+
+let dirpath_of_global = function
+  | ConstRef kn -> dirpath_of_mp (con_modpath kn)
+  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+    dirpath_of_mp (mind_modpath kn)
+  | VarRef _ -> empty_dirpath
+
+let qualid_of_global env r =
+  Libnames.make_qualid (dirpath_of_global r) (id_of_global env r)
+
+let safe_gen f env c =
+  let orig_extern_ref = Constrextern.get_extern_reference () in
+  let extern_ref loc vars r =
+    try orig_extern_ref loc vars r
+    with e when Errors.noncritical e ->
+      Libnames.Qualid (loc, qualid_of_global env r)
+  in
+  Constrextern.set_extern_reference extern_ref;
+  try
+    let p = f env c in
+    Constrextern.set_extern_reference orig_extern_ref;
+    p
+  with e when Errors.noncritical e ->
+    Constrextern.set_extern_reference orig_extern_ref;
+    str "??"
+
+let safe_pr_lconstr_env = safe_gen pr_lconstr_env
+let safe_pr_constr_env = safe_gen pr_constr_env
+let safe_pr_lconstr t = safe_pr_lconstr_env (Global.env()) t
+let safe_pr_constr t = safe_pr_constr_env (Global.env()) t
+
+
 (**********************************************************************)
 (* Global references *)
 
@@ -389,7 +447,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
 	| None ->
 	    let exl = Evarutil.non_instantiated sigma in
 	    if exl = [] then
-	      (str"No more subgoals."
+	      (str"No more subgoals." ++ fnl ()
 	       ++ emacs_print_dependent_evars sigma seeds)
 	    else
 	      let pei = pr_evars_int 1 exl in
@@ -415,7 +473,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
       v 0 (
 	int(List.length rest+1) ++ str" subgoals" ++
           str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
-	++ goals
+	++ goals ++ fnl ()
 	++ emacs_print_dependent_evars sigma seeds
       )
   | g1::rest,a::l ->
@@ -589,7 +647,7 @@ let pr_assumptionset env s =
 	str (string_of_mp mp ^ "." ^ string_of_label lab)
     in
     let safe_pr_ltype typ =
-      try str " : " ++ pr_ltype typ with _ -> mt ()
+      try str " : " ++ pr_ltype typ with e when Errors.noncritical e -> mt ()
     in
     let (vars,axioms,opaque) =
       ContextObjectMap.fold (fun t typ r ->
@@ -647,7 +705,6 @@ let pr_instance_gmap insts =
 
 (** Inductive declarations *)
 
-open Declarations
 open Termops
 open Reduction
 open Inductive
diff --git a/parsing/printer.mli b/parsing/printer.mli
index a034f0ed..3abe90e7 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -31,6 +31,17 @@ val pr_lconstr             : constr -> std_ppcmds
 val pr_constr_env          : env -> constr -> std_ppcmds
 val pr_constr              : constr -> std_ppcmds
 
+(** Same, but resilient to [Nametab] errors. Prints fully-qualified
+    names when [shortest_qualid_of_global] has failed. Prints "??"
+    in case of remaining issues (such as reference not in env). *)
+
+val safe_pr_lconstr_env         : env -> constr -> std_ppcmds
+val safe_pr_lconstr             : constr -> std_ppcmds
+
+val safe_pr_constr_env          : env -> constr -> std_ppcmds
+val safe_pr_constr              : constr -> std_ppcmds
+
+
 val pr_open_constr_env     : env -> open_constr -> std_ppcmds
 val pr_open_constr         : open_constr -> std_ppcmds
 
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))
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index dbc06856..77364180 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -188,11 +188,11 @@ let declare_tactic loc s cl =
                  Tacexpr.TacExtend($default_loc$,$se$,l)))
            | None -> () ])
           $atomic_tactics$
-      with e ->
+      with [ e when Errors.noncritical e ->
 	    Pp.msg_warning
 	      (Stream.iapp
 	        (Pp.str ("Exception in tactic extend " ^ $se$ ^": "))
-	        (Errors.print e));
+	        (Errors.print e)) ];
       Egrammar.extend_tactic_grammar $se$ $gl$;
       List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >>
     ])
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 4f39019f..bcdf7cff 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -55,11 +55,11 @@ let declare_command loc s nt cl =
   declare_str_items loc
     [ <:str_item< do {
 	try Vernacinterp.vinterp_add $se$ $funcl$
-	with e ->
+	with [ e when Errors.noncritical e ->
 	  Pp.msg_warning
 	    (Stream.iapp
 	       (Pp.str ("Exception in vernac extend " ^ $se$ ^": "))
-	       (Errors.print e));
+	       (Errors.print e)) ];
 	Egrammar.extend_vernac_command_grammar $se$ $nt$ $gl$
       } >> ]