aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/ide/bug4246.fake
blob: 16b552f6796188c48a8570dd4137805bb862b68d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
# first proof
ADD { Lemma a : True. }
ADD { Proof using. }
ADD here { trivial. } # first error
ADD { fail. }
ADD { Qed. }
WAIT
EDIT_AT here
# Fixing the proof
ADD { Qed. }
WAIT
EDIT_AT here
ADD { Qed. }
JOIN