From 6784ac890043adf62b4ed4ae3c027b28b3184ac7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 6 Dec 2018 20:53:05 +0100
Subject: [PATCH] Fix `iSimpl .. in ..`.

Thanks to @blaisorblade for reporting.
---
 tests/proofmode.ref               | 11 +++++++++++
 tests/proofmode.v                 |  4 ++++
 theories/proofmode/ltac_tactics.v |  4 ++--
 3 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index a3d7a44da..5d7abf860 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -74,6 +74,17 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   --------------------------------------∗
   â–·^(S n + S m) emp
   
+"test_iSimpl_in"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  x, y : nat
+  ============================
+  "H" : ⌜S (S (S x)) = y⌝
+  --------------------------------------∗
+  ⌜S (S (S x)) = y⌝
+  
 "test_iFrame_later_1"
      : string
 1 subgoal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index b71cbbf74..d395d97ab 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -412,6 +412,10 @@ Proof.
   done.
 Qed.
 
+Check "test_iSimpl_in".
+Lemma test_iSimpl_in x y : ⌜ (3 + x)%nat = y ⌝ -∗ ⌜ S (S (S x)) = y ⌝ : PROP.
+Proof. iIntros "H". iSimpl in "H". Show. done. Qed.
+
 Lemma test_iIntros_pure_neg : (⌜ ¬False ⌝ : PROP)%I.
 Proof. by iIntros (?). Qed.
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index c5d25de8f..837f91c71 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -119,8 +119,8 @@ Tactic Notation "iEval" tactic(t) "in" constr(H) :=
     |pm_reflexivity
     |].
 
-Tactic Notation "iSimpl" := iEval simpl.
-Tactic Notation "iSimpl" "in" constr(H) := iEval simpl in H.
+Tactic Notation "iSimpl" := iEval (simpl).
+Tactic Notation "iSimpl" "in" constr(H) := iEval (simpl) in H.
 
 (* It would be nice to also have an `iSsrRewrite`, however, for this we need to
 pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:
-- 
GitLab