test-suite/bugs/closed/3212.v


1
2
3
4
5
6
7
8
9
10

Lemma H : Prop = Prop.
reflexivity.
Qed.

Lemma foo : match H in (_ = X) return X with
  | eq_refl => True
end.
Proof.
Fail destruct H.
Abort.