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.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
