blob: aced9615eef4c2a16b2c11e261d991bf7bf7052e (
plain)
1
2
3
4
|
Require Import Coq.Program.Tactics.
Class Foo := { bar : Type }.
Fail Lemma foo : Foo -> bar. (* 'Command has indeed failed.' in both 8.4 and trunk *)
Fail Program Lemma foo : Foo -> bar.
|