From 8ca2bf371734817af4eb1fcdcade1d95f73ce9e2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Apr 2016 13:18:16 +0200
Subject: [PATCH] Tweak test file.

---
 tests/proofmode.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 8a02f7c9f..288c75c67 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -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
-- 
GitLab