blob: 7a1dc81e0bcdd2875a1f4b084df06d469d8e687f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
# 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. }
# QUERY { Stm PrintDag. }
# QUERY { Stm Finish. }
QUERY { Print d. }
QUERY { Check e. }
|
