# Script simulating a dialog between coqide and coqtop -ideslave
# Run it via fake_ide
#
# Test backtracking in presence of nested proofs
# Fifth, undo from an inner proof to a previous inner proof
#
INTERP Lemma aa : True -> True /\ True.
INTERP intro H.
INTERP split.
INTERP Lemma bb : False -> False.
INTERP intro H.
INTERP apply H.
INTERP Qed.
INTERP apply H.
INTERP Lemma cc : False -> True.
INTERP intro H.
INTERP destruct H.
REWIND 6
# We should be just before "Lemma bb"
# <replay>
INTERP Lemma bb : False -> False.
INTERP intro H.
INTERP apply H.
INTERP Qed.
INTERP apply H.
INTERP Lemma cc : False -> True.
INTERP intro H.
INTERP destruct H.
# </replay>
INTERP Qed.
INTERP apply H.
INTERP Qed.
INTERPRAW Fail idtac.
INTERPRAW Check (aa,bb,cc).