Commit 8ca2bf37 authored by Robbert Krebbers's avatar Robbert Krebbers

Tweak test file.

parent 194b69cd
Pipeline #505 failed with stage
......@@ -43,4 +43,4 @@ Qed.
Lemma demo_3 (M : cmraT) (P1 P2 P3 : uPred M) :
(P1 P2 P3) ( P1 (P2 x, (P3 x = 0) P3)).
Proof. iIntros "($ & $ & H)". iFrame "H". simpl. iNext. by iExists 0. Qed.
\ No newline at end of file
Proof. iIntros "($ & $ & H)". iFrame "H". iNext. by iExists 0. Qed.
\ No newline at end of file
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment