diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-06-09 13:30:35 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-06-09 13:30:35 +0200 |
| commit | fbfc1b8d6e9d95fcbacd3f4ab4921d6f3b01198e (patch) | |
| tree | 75417b1dfa1720e28c265105a06e3fb23dc85847 /test-suite/ide | |
| parent | a7a1ec22bc2aa06cc419f7012863656c3aec5871 (diff) | |
STM: states coming from workers have no proof terminators (Close #4246)
Hence we reuse the ones in master.
Diffstat (limited to 'test-suite/ide')
| -rw-r--r-- | test-suite/ide/bug4246.fake | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/ide/bug4246.fake b/test-suite/ide/bug4246.fake new file mode 100644 index 000000000..16b552f67 --- /dev/null +++ b/test-suite/ide/bug4246.fake @@ -0,0 +1,14 @@ +# first proof +ADD { Lemma a : True. } +ADD { Proof using. } +ADD here { trivial. } # first error +ADD { fail. } +ADD { Qed. } +WAIT +EDIT_AT here +# Fixing the proof +ADD { Qed. } +WAIT +EDIT_AT here +ADD { Qed. } +JOIN |