diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-11-26 18:09:53 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-11-26 18:09:53 +0100 |
| commit | 11ccb7333c2a82d59736027838acaea2237e2402 (patch) | |
| tree | cee059831f84e8ec6b020f3a545a6d6c7ac803f2 /interp | |
| parent | 566a24e28924ad4a7dda99891dce3882e6db112c (diff) | |
Make the pretty printer resilient to incomplete nametab (progress on #4363).
The nametab in which the error message is printed is not the one in
which the error message happens.
This reveals a weakness in the fix_exn code: the fix_exn function should
be pure, while in some cases (like this one) uses the global state (the
nametab) to print a term in a pretty way (the shortest non-ambiguous name
for constants).
This patch makes the externalization phase (used by term printing)
resilient to an incomplete nametab, so that printing a term in the
wrong nametab does not mask the original error.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f57772ecb..5160f07af 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -147,8 +147,17 @@ let extern_evar loc n l = CEvar (loc,n,l) For instance, in the debugger the tables of global references may be inaccurate *) +let safe_shortest_qualid_of_global vars r = + try shortest_qualid_of_global vars r + with Not_found -> + match r with + | VarRef v -> make_qualid DirPath.empty v + | ConstRef c -> make_qualid DirPath.empty Names.(Label.to_id (con_label c)) + | IndRef (i,_) | ConstructRef ((i,_),_) -> + make_qualid DirPath.empty Names.(Label.to_id (mind_label i)) + let default_extern_reference loc vars r = - Qualid (loc,shortest_qualid_of_global vars r) + Qualid (loc,safe_shortest_qualid_of_global vars r) let my_extern_reference = ref default_extern_reference |