blob: ff66277e03b19d60582b044fca517e4a20a9ed82 (
plain)
1
2
3
4
5
6
7
8
9
10
|
Set Primitive Projections.
(* This proof was accepted in Coq 8.5 because the subterm specs were not
projected correctly *)
Inductive foo : Prop := mkfoo { proj1 : False -> foo; proj2 : (forall P : Prop, P -> P) }.
Fail Fixpoint loop (x : foo) : False :=
loop (proj2 x _ x).
Fail Definition bad : False := loop (mkfoo (fun x => match x with end) (fun _ x => x)).
|
