blob: 0d83ad25ac16a83af0ee36e5ea8e1b21fac3ab44 (
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
27
28
29
|
# Script simulating a dialog between coqide and coqtop -ideslave
# Run it via fake_ide
#
# jumping between broken proofs
# first proof
ADD { Lemma a : True. }
ADD { Proof using. }
ADD here { idtac. }
ADD { exact Ix. }
ADD { Qed. }
# second proof
ADD { Lemma b : True. }
ADD here2 { Proof using. }
ADD { exact Ix. }
ADD { Qed. }
# We wait all slaves and expect both proofs to fail
WAIT
# Going back to the error
EDIT_AT here2
# this is not implemented yet, all after here is erased
EDIT_AT here
# Fixing the proof
ADD { exact I. }
ADD last { Qed. }
ASSERT TIP last
# we are back at the end
QUERY { Check a. }
QUERY { Fail Check b. }
|
