From 35f5a3fce53c8517d897660df6b66294d8662e46 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 10 Apr 2014 19:45:30 +0200
Subject: better description of bug 3251

---
 test-suite/bugs/closed/3251.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/test-suite/bugs/closed/3251.v b/test-suite/bugs/closed/3251.v
index 8d05196b06..5a7ae2002b 100644
--- a/test-suite/bugs/closed/3251.v
+++ b/test-suite/bugs/closed/3251.v
@@ -4,7 +4,9 @@ Ltac foo := idtac.
 foo is defined
 foo is defined
 
-... that's fishy.  But E. Tassi tells me that it's correct, because it happens on two threads. *)
+... 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: *)
-- 
cgit v1.2.3