From 0b2e6fe634da336ed34dec93072e847a1736afd2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 5 Nov 2017 10:47:15 +0100
Subject: Fixing a cause of failure of evar_map printer in debugger.

Indeed, the debugger debugs coqtop but it is itself just an ocaml
runtime extended with the coq printers. It does not know the
environment, so, looking in the Global.env() for the printers can only
fail.
---
 engine/namegen.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine')

diff --git a/engine/namegen.ml b/engine/namegen.ml
index a38c73ed0b..c548fc4ac9 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 ->
-- 
cgit v1.2.3


From 1f7a49374aa2e7a67d1326d02d0d6fb519427ee3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 5 Nov 2017 10:58:03 +0100
Subject: Preventively protect locally against failures of evar_map printer.

It is not clear that this is really needed, but in case it happens,
one will at least have a partial result available rather than an
unexploitable global failure of the parser.
---
 engine/termops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine')

diff --git a/engine/termops.ml b/engine/termops.ml
index b7fa2dc4a4..0f84d7868a 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
 
-- 
cgit v1.2.3


From 9f17cd59b801f42a2ca15cbc5e38de9c8be42312 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 5 Nov 2017 11:00:16 +0100
Subject: Cosmetic changes in evar_map printer.

---
 engine/termops.ml | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

(limited to 'engine')

diff --git a/engine/termops.ml b/engine/termops.ml
index 0f84d7868a..76f707f945 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -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
-- 
cgit v1.2.3