blob: 5ecf280153f5c438d55bca2875f6489e4ea193a9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
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.
|
