|
Goal True.
idtac.
Ltac foo := idtac.
(* print out happens twice:
foo is defined
foo is defined
... that's fishy. But E. Tassi tells me that it's expected since "Ltac" generates a side
effect that escapes the proof. In the STM model this means the command is executed twice,
once in the proof branch, and another time in the main branch *)
Undo.
Ltac foo := idtac.
(* Before 5b39c3535f7b3383d89d7b844537244a4e7c0eca, this would print out: *)
(* Anomaly: Backtrack.backto to a state with no vcs_backup. Please report. *)
Abort.
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.17Angebot
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
|
