diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-03-27 19:20:01 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-03-27 19:44:04 +0200 |
| commit | 076efd5f8d17f1b73bcc7669641b89f86819e3c9 (patch) | |
| tree | 919af6e55aa85ef4c0dcb213335ddd980b6fe2d6 /test-suite/ide | |
| parent | c1dcb97cf95c10d19f67689108da8726232da4fb (diff) | |
stm: don't propagate side effects when editing a proof
Diffstat (limited to 'test-suite/ide')
| -rw-r--r-- | test-suite/ide/bug7088.fake | 13 |
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 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 + |