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

about summary refs log tree commit diff homepage

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

blob: e86b3be64e468047a95996b76bd6b0f712cf85d2 (plain)

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

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