blob: c29e529783e07da5f1df4d9ba4e429cdbcfde2a2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* This used to fail in Coq version 8.1 beta due to a non variable
universe (issued by the inductive sort-polymorphism) being sent by
pretyping to the kernel (bug #1182) *)
Variable T : Type.
Variable x : nat*nat.
Check let (_, _) := x in sigT (fun _ : T => nat).
(* This used to raise an anomaly in V8.4, up to pl2 *)
Goal {x: nat & x=x}.
Fail exists (fun x =>
match
projT2 (projT2 x) as e in (_ = y)
return _ = existT _ (projT1 x) (existT _ y e)
with
| eq_refl => eq_refl
end).
|
