Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_3382.v Sprache: Coq

Original von: Coq^©

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.

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

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.