From 5cff8a26e6444a4523eb8f471a1203a33c611b5b Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 21 Mar 2013 21:11:17 +0000
Subject: Robust display of NotConvertibleTypeField errors (fix #3008, #2995)

 Since the nametab isn't aware of everything needed to print mismatched
 types (cf the bug test-cases), we create a robust term printer that
 known how to print a fully-qualified name when [shortest_qualid_of_global]
 has failed. These Printer.safe_pr_constr and alii are meant to never fail
 (at worse they display "??", for instance when the env isn't rich enough).

 Moreover, the environnement may have changed between the raise
 of NotConvertibleTypeField and its display, so we store the original
 env in the exception.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16342 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml  | 23 ++++++++++++-----------
 interp/constrextern.mli |  9 ++++++---
 2 files changed, 18 insertions(+), 14 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 47753c1582..84baefe615 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -140,20 +140,21 @@ let insert_pat_alias loc p = function
 let extern_evar loc n l =
   if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None)
 
-let debug_global_reference_printer =
-  ref (fun _ -> failwith "Cannot print a global reference")
+(** We allow customization of the global_reference printer.
+    For instance, in the debugger the tables of global references
+    may be inaccurate *)
 
-let in_debugger = ref false
+let default_extern_reference loc vars r =
+  Qualid (loc,shortest_qualid_of_global vars r)
 
-let set_debug_global_reference_printer f =
-  debug_global_reference_printer := f
+let my_extern_reference = ref default_extern_reference
 
-let extern_reference loc vars r =
-  if !in_debugger then
-    (* Debugger does not have the tables of global reference at hand *)
-    !debug_global_reference_printer loc r
-  else
-    Qualid (loc,shortest_qualid_of_global vars r)
+let set_extern_reference f = my_extern_reference := f
+let get_extern_reference () = !my_extern_reference
+
+let extern_reference loc vars l = !my_extern_reference loc vars l
+
+let in_debugger = ref false
 
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 0e40e83e67..0a4192c3ea 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -51,9 +51,12 @@ val print_universes : bool ref
 val print_no_symbol : bool ref
 val print_projections : bool ref
 
-(** Debug printing options *)
-val set_debug_global_reference_printer :
-  (Loc.t -> global_reference -> reference) -> unit
+(** Customization of the global_reference printer *)
+val set_extern_reference :
+  (Loc.t -> Id.Set.t -> global_reference -> reference) -> unit
+val get_extern_reference :
+  unit -> (Loc.t -> Id.Set.t -> global_reference -> reference)
+
 val in_debugger : bool ref
 
 (** This governs printing of implicit arguments. If [with_implicits] is
-- 
cgit v1.2.3