diff options
author | 2013-03-21 21:11:17 +0000 | |
---|---|---|
committer | 2013-03-21 21:11:17 +0000 | |
commit | 5cff8a26e6444a4523eb8f471a1203a33c611b5b (patch) | |
tree | a6cdc580245c6390deb7f7b26f86bf60fe9e9a15 /test-suite/bugs | |
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 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2995.v | 9 | ||||
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/3008.v | 29 |
2 files changed, 38 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2995.v b/test-suite/bugs/closed/shouldsucceed/2995.v new file mode 100644 index 000000000..ba3acd088 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2995.v @@ -0,0 +1,9 @@ +Module Type Interface. + Parameter error: nat. +End Interface. + +Module Implementation <: Interface. + Definition t := bool. + Definition error: t := false. +Fail End Implementation. +(* A UserError here is expected, not an uncaught Not_found *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/3008.v b/test-suite/bugs/closed/shouldsucceed/3008.v new file mode 100644 index 000000000..3f3a979a3 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/3008.v @@ -0,0 +1,29 @@ +Module Type Intf1. +Parameter T : Type. +Inductive a := A. +End Intf1. + +Module Impl1 <: Intf1. +Definition T := unit. +Inductive a := A. +End Impl1. + +Module Type Intf2 + (Impl1 : Intf1). +Parameter x : Impl1.A=Impl1.A -> Impl1.T. +End Intf2. + +Module Type Intf3 + (Impl1 : Intf1) + (Impl2 : Intf2(Impl1)). +End Intf3. + +Fail Module Toto + (Impl1' : Intf1) + (Impl2 : Intf2(Impl1')) + (Impl3 : Intf3(Impl1)(Impl2)). +(* A UserError is expected here, not an uncaught Not_found *) + +(* NB : the Inductive above and the A=A weren't in the initial test, + they are here only to force an access to the environment + (cf [Printer.qualid_of_global]) and check that this env is ok. *)
\ No newline at end of file |