From 076efd5f8d17f1b73bcc7669641b89f86819e3c9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 27 Mar 2018 19:20:01 +0200
Subject: stm: don't propagate side effects when editing a proof

---
 test-suite/ide/bug7088.fake | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/ide/bug7088.fake

(limited to 'test-suite/ide')

diff --git a/test-suite/ide/bug7088.fake b/test-suite/ide/bug7088.fake
new file mode 100644
index 000000000..e2a2aa52a
--- /dev/null
+++ b/test-suite/ide/bug7088.fake
@@ -0,0 +1,13 @@
+ADD { Arguments id T x : rename. }
+ADD { Lemma foo : True. }
+ADD here { Proof. }
+ADD { exact 3. }
+ADD { Qed. }
+WAIT
+EDIT_AT here
+ADD { Arguments id FOO BAR : rename. }
+ADD { exact I. }
+ADD { Qed. }
+ADD { Arguments id T x : assert. }
+JOIN
+
-- 
cgit v1.2.3