|
Ltac bar x := pose x.
Tactic Notation "foo" open_constr(x) := bar x.
Class baz := { baz' : Type }.
Goal True.
(* Original error was an anomaly which is fixed; now, it succeeds but
leaving an evar, while calling pose would not leave an evar, so I
guess it is still a bug in the sense that the semantics of pose is
not preserved *)
foo baz'.
Abort.
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.93Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
