Merge PR #6072: Protecting evar map printer

2 files changed, 22 insertions, 22 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index a38c73ed0..c548fc4ac 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -132,8 +132,8 @@ let hdchar env sigma c =
     | Cast (c,_,_) | App (c,_) -> hdrec k c
     | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn)))
     | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn))
-    | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x))
-    | Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x))
+    | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
+    | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
     | Var id  -> lowercase_first_char id
     | Sort s -> sort_hdchar (ESorts.kind sigma s)
     | Rel n ->
diff --git a/engine/termops.ml b/engine/termops.ml
index b7fa2dc4a..76f707f94 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -327,11 +327,11 @@ let pr_evar_constraints sigma pbs =
       Namegen.make_all_name_different env sigma
     in
     print_env_short env ++ spc () ++ str "|-" ++ spc () ++
-      print_constr_env env sigma (EConstr.of_constr t1) ++ spc () ++
+      protect (print_constr_env env sigma) (EConstr.of_constr t1) ++ spc () ++
       str (match pbty with
             | Reduction.CONV -> "=="
             | Reduction.CUMUL -> "<=") ++
-      spc () ++ print_constr_env env Evd.empty (EConstr.of_constr t2)
+      spc () ++ protect (print_constr_env env Evd.empty) (EConstr.of_constr t2)
   in
   prlist_with_sep fnl pr_evconstr pbs
 
@@ -358,37 +358,37 @@ let pr_evar_list sigma l =
     h 0 (str (string_of_existential ev) ++
       str "==" ++ pr_evar_info evi ++
       (if evi.evar_body == Evar_empty
-       then str " {" ++  pr_existential_key sigma ev ++ str "}"
+       then str " {" ++ pr_existential_key sigma ev ++ str "}"
        else mt ()))
   in
   h 0 (prlist_with_sep fnl pr l)
 
-let pr_evar_by_depth depth sigma = match depth with
-| None ->
-  (* Print all evars *)
-  let to_list d =
-    let open Evd in
-    (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *)
-    let l = ref [] in
-    let fold_def evk evi () = match evi.evar_body with
+let to_list d =
+  let open Evd in
+  (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *)
+  let l = ref [] in
+  let fold_def evk evi () = match evi.evar_body with
     | Evar_defined _ -> l := (evk, evi) :: !l
     | Evar_empty -> ()
-    in
-    let fold_undef evk evi () = match evi.evar_body with
+  in
+  let fold_undef evk evi () = match evi.evar_body with
     | Evar_empty -> l := (evk, evi) :: !l
     | Evar_defined _ -> ()
-    in
-    Evd.fold fold_def d ();
-    Evd.fold fold_undef d ();
-    !l
   in
-  str"EVARS:"++brk(0,1)++pr_evar_list sigma (to_list sigma)++fnl()
-| Some n ->
+  Evd.fold fold_def d ();
+  Evd.fold fold_undef d ();
+  !l
+
+let pr_evar_by_depth depth sigma = match depth with
+| None ->
   (* Print all evars *)
+  str"EVARS:" ++ brk(0,1) ++ pr_evar_list sigma (to_list sigma) ++ fnl()
+| Some n ->
+  (* Print closure of undefined evars *)
   str"UNDEFINED EVARS:"++
   (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++
   brk(0,1)++
-  pr_evar_list sigma (evar_dependency_closure n sigma)++fnl()
+  pr_evar_list sigma (evar_dependency_closure n sigma) ++ fnl()
 
 let pr_evar_by_filter filter sigma =
   let open Evd in