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

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