diff options
Diffstat (limited to 'library/nametab.ml')
| -rw-r--r-- | library/nametab.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 9f2bede75..fd27ef264 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -522,8 +522,8 @@ let pr_global_env env ref = (* Il est important de laisser le let-in, car les streams s'évaluent paresseusement : il faut forcer l'évaluation pour capturer l'éventuelle levée d'une exception (le cas échoit dans le debugger) *) - let s = string_of_qualid (shortest_qualid_of_global env ref) in - (str s) + try str (string_of_qualid (shortest_qualid_of_global env ref)) + with Not_found as e -> prerr_endline "pr_global_env not found"; raise e let global_inductive r = match global r with |