diff options
| author | letouzey | 2013-03-21 21:11:17 +0000 |
|---|---|---|
| committer | letouzey | 2013-03-21 21:11:17 +0000 |
| commit | 5cff8a26e6444a4523eb8f471a1203a33c611b5b (patch) | |
| tree | a6cdc580245c6390deb7f7b26f86bf60fe9e9a15 /dev | |
| parent | 4da7ddb8c3c2f1dafd5d9187741659a9332b75c2 (diff) | |
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
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 4 | ||||
| -rw-r--r-- | dev/top_printers.ml | 6 |
2 files changed, 5 insertions, 5 deletions
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) |