blob: 770350fbdc3d4fcfea29ef1aaf30538054afb184 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
# Script simulating a dialog between coqide and coqtop -ideslave
# Run it via fake_ide
#
# Undoing declarations, as first step
# new in 8.2
#
ADD { Theorem d : O=O. }
ADD here { Definition e := O. }
ADD { Definition f := O. }
# This is a bug in Stm undo, e is lost from master
EDIT_AT here
ADD { Definition f := O. }
ADD { assert True by trivial. }
ADD { exact (eq_refl e). }
ADD { Qed. }
ADD { Stm PrintDag. }
ADD { Stm Finish. }
QUERY { Print d. }
QUERY { Check e. }
|
