aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4273.v
blob: 591ea4b5b2ccac5740dcfb66acf2b63e40769ad3 (plain)
1
2
3
4
5
6
7
8
9

  
Set Primitive Projections.
Record total2 (P : nat -> Prop) := tpair { pr1 : nat; pr2 : P pr1 }.
Theorem onefiber' (q : total2 (fun y => y = 0)) : True.
Proof. assert (foo:=pr2 _ q). simpl in foo.
       destruct foo. (* Error: q is used in conclusion. *) exact I. Qed.

Print onefiber'.