From e47c73d8fdddec6adc3981bf6a23c710a9835222 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 14 Jun 2019 17:12:56 +0200
Subject: [PATCH] Fix parsing precedence for iEval

---
 tests/proofmode.ref               | 2 +-
 tests/proofmode.v                 | 7 +++++++
 theories/proofmode/ltac_tactics.v | 4 ++--
 3 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index e1ab0ee88..b50195bf3 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -126,7 +126,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iSimpl in (constr)",
-"iEval (tactic) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
+"iEval (tactic3) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
 last call failed.
 Tactic failure: iEval: %: unsupported selection pattern.
 "test_iFrame_later_1"
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 515cb9dbd..f1b43337b 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -480,6 +480,13 @@ Proof.
   done.
 Qed.
 
+Lemma test_iEval_precedence : True ⊢ True : PROP.
+Proof.
+  iIntros.
+  (* Ensure that in [iEval (a); b], b is not parsed as part of the argument of [iEval]. *)
+  iEval (rewrite /=); iPureIntro; exact I.
+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.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index dff46653b..2d055b316 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -195,7 +195,7 @@ Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
   iClear Hs; clear xs.
 
 (** ** Simplification *)
-Tactic Notation "iEval" tactic(t) :=
+Tactic Notation "iEval" tactic3(t) :=
   iStartProof;
   eapply tac_eval;
     [let x := fresh in intros x; t; unfold x; reflexivity
@@ -212,7 +212,7 @@ Local Ltac iEval_go t Hs :=
       |pm_reduce; iEval_go t Hs]
   end.
 
-Tactic Notation "iEval" tactic(t) "in" constr(Hs) :=
+Tactic Notation "iEval" tactic3(t) "in" constr(Hs) :=
   iStartProof; let Hs := iElaborateSelPat Hs in iEval_go t Hs.
 
 Tactic Notation "iSimpl" := iEval (simpl).
-- 
GitLab