# 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. }