diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-10-06 19:34:28 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-10-06 19:34:28 +0200 |
| commit | fd39a2e844f93b314c2f0b78510f0573cfa1bef3 (patch) | |
| tree | d31080bea8310cdd91d5f13fb74c666d53dfdd86 /interp | |
| parent | 0a6f0c161756a1878dd81e438df86f08631d8399 (diff) | |
Revert "Make the pretty printer resilient to incomplete nametab (progress on #4363)."
This reverts commit 11ccb7333c2a82d59736027838acaea2237e2402.
This fixes bug #4874. We fallback to the original error message of v8.4.
The fallback printer introduced in this commit only gave unqualified names,
which is what this bug reports.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 68a3cf0f4..ae9b5bace 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -147,17 +147,8 @@ 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,safe_shortest_qualid_of_global vars r) + Qualid (loc,shortest_qualid_of_global vars r) let my_extern_reference = ref default_extern_reference |