diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-05 10:47:15 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-05 10:47:20 +0100 |
| commit | 0b2e6fe634da336ed34dec93072e847a1736afd2 (patch) | |
| tree | a520f907d9eea30650876fc706be378108ee68a6 /engine/namegen.ml | |
| parent | f281a8a88e8fc7c41cc5680db2443d9da33b47b7 (diff) | |
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.
Diffstat (limited to 'engine/namegen.ml')
| -rw-r--r-- | engine/namegen.ml | 4 |
1 files changed, 2 insertions, 2 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 -> |