summaryrefslogtreecommitdiff
path: root/test-suite/ide/bug7088.fake
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/ide/bug7088.fake')
-rw-r--r--test-suite/ide/bug7088.fake13
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/ide/bug7088.fake b/test-suite/ide/bug7088.fake
new file mode 100644
index 00000000..e2a2aa52
--- /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
+