From 84d73de1dfb77667b752f888d8e519f0644eb9f0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 10 Nov 2019 16:55:19 +0100
Subject: [PATCH] Fix issue pointed out by @tchajed in
 https://gitlab.mpi-sws.org/iris/iris/merge_requests/330#note_41322

---
 tests/proofmode_iris.v            | 5 +++++
 theories/proofmode/ltac_tactics.v | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index d369d746b..c2998995f 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -220,6 +220,11 @@ Section iris_tests.
     iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)".
     eauto.
   Qed.
+
+  Theorem test_iApply_inG `{!inG Σ A} γ (x x' : A) :
+    x' ≼ x →
+    own γ x -∗ own γ x'.
+  Proof. intros. by iApply own_mono. Qed.
 End iris_tests.
 
 Section monpred_tests.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 6edfd4516..fbde9ca80 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -70,7 +70,7 @@ Tactic Notation "iStartProof" :=
   | |- envs_entails _ _ => idtac
   | |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
                [iSolveTC || fail "iStartProof: not a BI assertion"
-               |apply tac_start]
+               |notypeclasses refine (tac_start _ _)]
   end.
 
 (* Same as above, with 2 differences :
-- 
GitLab