Merge PR #6072: Protecting evar map printer

1 files changed, 20 insertions, 20 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index b7fa2dc4a4..76f707f945 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