# Script simulating a dialog between coqide and coqtop -ideslave
# Run it via fake_ide
#
# Bug 2082
# Broken due to proof engine rewriting
#
INTERP Variable A : Prop.
INTERP Variable B : Prop.
INTERP Axiom OR : A \/ B.
INTERP Lemma MyLemma2 : True.
INTERP proof.
INTERP per cases of (A \/ B) by OR.
INTERP suppose A.
INTERP then (1 = 1).
INTERP then H1 : thesis.
INTERP thus thesis by H1.
INTERP suppose B.
REWIND 1
#
INTERP suppose B.
#
REWIND 2
#
INTERP thus thesis by H1.
INTERP suppose B.
#
INTERP then (1 = 1).
INTERP then H2 : thesis.
INTERP thus thesis by H2.
INTERP end cases.
INTERP end proof.
INTERP Qed.