From ea14f64dc03e66d05dd18d5b2a52cdd3c1314f2b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Jun 2016 17:13:39 +0200
Subject: [PATCH] Make iAssert infer the cmra M of the asserted uPred M.

---
 proofmode/tactics.v          | 4 ++--
 tests/joining_existentials.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index ce0289e4a..b076e5b79 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -713,7 +713,7 @@ Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
               ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }).
 
 (** * Assert *)
-Tactic Notation "iAssert" constr(Q) "with" constr(Hs) "as" constr(pat) :=
+Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
   let H := iFresh in
   let Hs := spec_pat.parse Hs in
   lazymatch Hs with
@@ -735,7 +735,7 @@ Tactic Notation "iAssert" constr(Q) "with" constr(Hs) "as" constr(pat) :=
   | ?pat => fail "iAssert: invalid pattern" pat
   end.
 
-Tactic Notation "iAssert" constr(Q) "as" constr(pat) :=
+Tactic Notation "iAssert" open_constr(Q) "as" constr(pat) :=
   iAssert Q with "[]" as pat.
 
 (** * Rewrite *)
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index e637415fd..b95c6bb0e 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -53,7 +53,7 @@ Lemma Q_res_join γ : barrier_res γ Ψ1 ★ barrier_res γ Ψ2 ⊢ ▷ barrier_
 Proof.
   iIntros "[Hγ Hγ']";
   iDestruct "Hγ" as {x} "[#Hγ Hx]"; iDestruct "Hγ'" as {x'} "[#Hγ' Hx']".
-  iAssert (▷ (x ≡ x'):iProp)%I as "Hxx" .
+  iAssert (▷ (x ≡ x'))%I as "Hxx" .
   { 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.
-- 
GitLab