blob: aa1d9bb2a72a2fc5ddf8aadffff9bab15c551b68 (
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
|
# Script simulating a dialog between coqide and coqtop -ideslave
# Run it via fake_ide
#
# focusing a broken proof and fixing it
# first proof
ADD { Lemma a : True. }
ADD { Proof using. }
ADD here { idtac. }
ADD { exact Ix. }
ADD { Qed. }
# second proof
ADD { Lemma b : False. }
ADD { Proof using. }
ADD { give_up. }
ADD last { Admitted. }
# We join and expect some proof to fail
WAIT
# Going back to the error
EDIT_AT here
# Fixing the proof
ADD { exact I. }
ADD { Qed. }
# we are back at the end
ASSERT TIP last
QUERY { Check a. }
QUERY { Check b. }
|
