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.mli | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'interp/constrextern.mli') diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 0e40e83e6..0a4192c3e 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