From 79df624d72204c21fb3a8b5da71fddfb8804abbe Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 8 Jun 2016 10:04:06 -0400
Subject: [PATCH] Small clean up.

---
 tests/joining_existentials.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index b95c6bb0e..340897569 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -57,8 +57,8 @@ Proof.
   { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
     rewrite own_valid csum_validI /= agree_validI agree_equivI later_equivI /=.
     rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
-    rewrite (ne_proper (cFunctor_map G) (cid, cid) (_ â—Ž _, _ â—Ž _)).
-    2:by split; intro; simpl; symmetry; apply iProp_fold_unfold.
+    rewrite (ne_proper (cFunctor_map G) (cid, cid) (_ â—Ž _, _ â—Ž _)); last first.
+    { by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
     rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". }
   iNext. iRewrite -"Hxx" in "Hx'".
   iExists x; iFrame "Hγ". iApply Ψ_join; by iSplitL "Hx".
-- 
GitLab