blob: a50572ace075f22dac710077f2831cf122fbcc3b (
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.
|