blob: f9b29ca1854b82c96c296ab12086a036d340a660 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
# Script simulating a dialog between coqide and coqtop -ideslave
# Run it via fake_ide
#
# Test backtracking in presence of nested proofs
# First, undoing the whole
#
INTERP Lemma aa : True -> True /\ True.
INTERP intro H.
INTERP split.
INTERP Lemma bb : False -> False.
INTERP intro H.
INTERP apply H.
INTERP Qed.
INTERP apply H.
INTERP Lemma cc : False -> True.
INTERP intro H.
INTERP destruct H.
INTERP Qed.
INTERP apply H.
INTERP Qed.
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.
|
