From 11ccb7333c2a82d59736027838acaea2237e2402 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 26 Nov 2015 18:09:53 +0100
Subject: 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.
---
 interp/constrextern.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f57772ecb0..5160f07af0 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
 
-- 
cgit v1.2.3