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 ++--
 dev/top_printers.ml | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'dev')

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
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index db895fc0f7..ec9c0a95ee 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -454,7 +454,7 @@ let encode_path loc prefix mpdir suffix id =
   Qualid (loc, make_qualid
     (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id)
 
-let raw_string_of_ref loc = function
+let raw_string_of_ref loc _ = function
   | ConstRef cst ->
       let (mp,dir,id) = repr_con cst in
       encode_path loc "CST" (Some (mp,dir)) [] (Label.to_id id)
@@ -470,7 +470,7 @@ let raw_string_of_ref loc = function
   | VarRef id ->
       encode_path loc "SECVAR" None [] id
 
-let short_string_of_ref loc = function
+let short_string_of_ref loc _ = function
   | VarRef id -> Ident (loc,id)
   | ConstRef cst -> Ident (loc,Label.to_id (pi3 (repr_con cst)))
   | IndRef (kn,0) -> Ident (loc,Label.to_id (pi3 (repr_mind kn)))
@@ -486,5 +486,5 @@ let short_string_of_ref loc = function
    pretty-printer should not make calls to the global env since ocamldebug
    runs in a different process and does not have the proper env at hand *)
 let _ = Constrextern.in_debugger := true
-let _ = Constrextern.set_debug_global_reference_printer
+let _ = Constrextern.set_extern_reference
   (if !rawdebug then raw_string_of_ref else short_string_of_ref)
-- 
cgit v1.2.3