diff options
| author | Maxime Dénès | 2017-11-06 13:29:41 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-06 13:29:41 +0100 |
| commit | e029cf5b417b22ebc65a8193469bbbe450f725ce (patch) | |
| tree | 0edab9cd79e86225f7df9646659e64f6b17a41ef /engine/namegen.ml | |
| parent | 9805457c2f63c27a281a2b8bbbaa771e4b695f68 (diff) | |
| parent | 9f17cd59b801f42a2ca15cbc5e38de9c8be42312 (diff) | |
Merge PR #6072: Protecting evar map printer
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 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 -> |