931.v « closed « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

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

blob: ea3347a8517c593b7fcb10ffd09e2c9c41fce8e0 (plain)

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

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