From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/3373.v | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 test-suite/bugs/closed/3373.v (limited to 'test-suite/bugs/closed/3373.v') 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. -- cgit v1.2.3