Imported Upstream version 8.5~beta1+dfsg

1 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3251.v b/test-suite/bugs/closed/3251.v
new file mode 100644
index 00000000..5a7ae200
--- /dev/null
+++ b/test-suite/bugs/closed/3251.v
@@ -0,0 +1,13 @@
+Goal True.
+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. *)