931.v « shouldsucceed « closed « bugs « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/bugs/closed/shouldsucceed/931.v

blob: 21f15e721880c26179dcb5dae7cccf3434acb1d7 (plain)

Parameter P : forall n : nat, n=n -> Prop.

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