diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/bugs/closed/3373.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/bugs/closed/3373.v')
-rw-r--r-- | test-suite/bugs/closed/3373.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3373.v b/test-suite/bugs/closed/3373.v new file mode 100644 index 00000000..5ecf2801 --- /dev/null +++ b/test-suite/bugs/closed/3373.v @@ -0,0 +1,33 @@ +(* File reduced by coq-bug-finder from original input, then from 5968 lines to +11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 +lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then +from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 +lines to 320 lines, then from 328 lines to 302 lines, then from 332 lines to 21 +lines *) +Set Universe Polymorphism. +Module short. + Record foo := { bar : Type }. + Coercion baz (x : foo@{Set}) : Set := bar x. + Goal True. + Proof. + Fail pose ({| bar := Set |} : Type). (* check that it fails *) + try pose ({| bar := Set |} : Type). (* Anomaly: apply_coercion_args: mismatch between arguments and coercion. +Please report. *) + Admitted. +End short. + +Module long. + Axiom admit : forall {T}, T. + Definition UU := Set. + Definition UU' := Type. + Definition hSet:= sigT (fun X : UU' => admit) . + Definition pr1hSet:= @projT1 UU (fun X : UU' => admit) : hSet -> Type. + Coercion pr1hSet: hSet >-> Sortclass. + Axiom binop : UU -> Type. + Axiom setwithbinop : Type. + Goal True. + Proof. + Fail pose (( @projT1 _ ( fun X : hSet@{i j k} => binop X ) ) : _ -> hSet). (* check that it fails *) + try pose (( @projT1 _ ( fun X : hSet@{i j k} => binop X ) ) : _ -> hSet). (* check that it's not an anomaly *) + Admitted. +End long. |