aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/931.v
blob: e86b3be64e468047a95996b76bd6b0f712cf85d2 (plain)
1
2
3
4
5
6
7
Parameter P : forall n : nat, n=n -> Prop.

Goal Prop.
  refine (P _ _).
  2:instantiate (1:=0).
  trivial.
Qed.