bug_13131.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

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

blob: b358ae3eccfea03bef24d41e7a8c557ba89ea864 (plain)

Set Mangle Names.

Class A := {}.

Lemma foo `{A} : A.
Proof. Fail exact H. assumption. Qed.