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 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 58bfe08322..a050e45c38 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -24,6 +24,9 @@ open Cases open Logic open Printer open Evd +open Libnames +open Globnames +open Declarations let pr_lconstr c = quote (pr_lconstr c) let pr_lconstr_env e c = quote (pr_lconstr_env e c) @@ -598,9 +601,11 @@ let explain_not_match_error = function str "types given to " ++ str (Id.to_string id) ++ str " differ" | NotConvertibleBodyField -> str "the body of definitions differs" - | NotConvertibleTypeField (typ1, typ2) -> - str "expected type" ++ spc () ++ pr_lconstr typ2 ++ spc () ++ - str "but found type" ++ spc () ++ pr_lconstr typ1 + | NotConvertibleTypeField (env, typ1, typ2) -> + str "expected type" ++ spc () ++ + quote (Printer.safe_pr_lconstr_env env typ2) ++ spc () ++ + str "but found type" ++ spc () ++ + quote (Printer.safe_pr_lconstr_env env typ1) | NotSameConstructorNamesField -> str "constructor names differ" | NotSameInductiveNameInBlockField -> |