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