diff options
| author | gareuselesinge | 2013-08-08 18:52:13 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-08-08 18:52:13 +0000 |
| commit | a936e9ae133f103ed9f781a7aa363c0006a2f178 (patch) | |
| tree | 6fc689fc24f3c8909dad28a46578dc9c3456f65d /test-suite | |
| parent | 2b9bc762ae31266212e7ab2defec7df41b08b6f8 (diff) | |
Coqide ported to STM
Main changes for STM:
1) protocol changed to carry edit/state ids
2) colouring reflects the actual status of every span (evaluated or not)
3) button to force the evaluation of the whole buffer
4) cmd_stack and backtracking completely changed to use state numbers
instead of counting sentences
5) feedback messages are completely asynchronous, and the whole protocol
could be made so with a minor effort, but there is little point in it
right now. Left as a future improvement. Missing bit: add
sentence-id to responses of interp command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16677 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ide/undo012.fake | 4 | ||||
| -rw-r--r-- | test-suite/ide/undo013.fake | 3 | ||||
| -rw-r--r-- | test-suite/ide/undo016.fake | 2 |
3 files changed, 2 insertions, 7 deletions
diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake index f9b29ca185..49169eba82 100644 --- a/test-suite/ide/undo012.fake +++ b/test-suite/ide/undo012.fake @@ -22,5 +22,5 @@ REWIND 1 # We should now be just before aa, without opened proofs INTERPRAW Fail idtac. INTERPRAW Fail Check aa. -INTERPRAW Fail Check bb. -INTERPRAW Fail Check cc. +INTERPRAW Check bb. +INTERPRAW Check cc. diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake index 3b1c61e66d..389da27650 100644 --- a/test-suite/ide/undo013.fake +++ b/test-suite/ide/undo013.fake @@ -20,9 +20,6 @@ INTERP apply H. REWIND 2 # We should now be just before "Lemma cc" # <replay> -INTERP Lemma cc : False -> True. -INTERP intro H. -INTERP destruct H. INTERP Qed. INTERP apply H. # </replay> diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake index 2a6e512cb7..a188e31b1f 100644 --- a/test-suite/ide/undo016.fake +++ b/test-suite/ide/undo016.fake @@ -18,8 +18,6 @@ INTERP destruct H. REWIND 6 # We should be just before "Lemma bb" # <replay> -INTERP Lemma bb : False -> False. -INTERP intro H. INTERP apply H. INTERP Qed. INTERP apply H. |