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
---
 dev/base_include | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index c75413a386..ca40f5f7af 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -210,8 +210,8 @@ let pf_e gl s =
 
 (* Set usual printing since the global env is available from the tracer *)
 let _ = Constrextern.in_debugger := false
-let _ = Constrextern.set_debug_global_reference_printer
-  (fun loc r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
+let _ = Constrextern.set_extern_reference
+  (fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
 
 open Toplevel
 let go = loop
-- 
cgit v1.2.3