From c71ad286709931da0abf5b93dd7c1330efb24a93 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 29 Apr 2016 22:39:37 +0200
Subject: [PATCH] Make iRewrite work with terms with arguments and
 spec_patterns.

---
 proofmode/tactics.v | 22 ++++++++++++----------
 tests/proofmode.v   | 10 ++++++++++
 2 files changed, 22 insertions(+), 10 deletions(-)

diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index eaceb0d23..ab409612e 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -703,18 +703,20 @@ Local Ltac iRewriteFindPred :=
      match goal with |- (∀ y, @?Ψ y ⊣⊢ _) => unify Φ Ψ; reflexivity end
   end.
 
-Local Tactic Notation "iRewriteCore" constr(lr) constr(Heq) :=
+Local Tactic Notation "iRewriteCore" constr(lr) open_constr(t) :=
+  let Heq := iFresh in iPoseProof t as Heq; last (
   eapply (tac_rewrite _ Heq _ _ lr);
     [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
     |let P := match goal with |- ?P ⊢ _ => P end in
      reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
     |iRewriteFindPred
-    |intros ??? ->; reflexivity|lazy beta].
+    |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
 
-Tactic Notation "iRewrite" constr(Heq) := iRewriteCore false Heq.
-Tactic Notation "iRewrite" "-" constr(Heq) := iRewriteCore true Heq.
+Tactic Notation "iRewrite" open_constr(t) := iRewriteCore false t.
+Tactic Notation "iRewrite" "-" open_constr(t) := iRewriteCore true t.
 
-Local Tactic Notation "iRewriteCore" constr(lr) constr(Heq) "in" constr(H) :=
+Local Tactic Notation "iRewriteCore" constr(lr) open_constr(t) "in" constr(H) :=
+  let Heq := iFresh in iPoseProof t as Heq; last (
   eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
     [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
     |env_cbv; reflexivity || fail "iRewrite:" H "not found"
@@ -722,12 +724,12 @@ Local Tactic Notation "iRewriteCore" constr(lr) constr(Heq) "in" constr(H) :=
      reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
     |iRewriteFindPred
     |intros ??? ->; reflexivity
-    |env_cbv; reflexivity|lazy beta].
+    |env_cbv; reflexivity|lazy beta; iClear Heq]).
 
-Tactic Notation "iRewrite" constr(Heq) "in" constr(H) :=
-  iRewriteCore false Heq in H.
-Tactic Notation "iRewrite" "-" constr(Heq) "in" constr(H) :=
-  iRewriteCore true Heq in H.
+Tactic Notation "iRewrite" open_constr(t) "in" constr(H) :=
+  iRewriteCore false t in H.
+Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
+  iRewriteCore true t in H.
 
 (* Make sure that by and done solve trivial things in proof mode *)
 Hint Extern 0 (of_envs _ ⊢ _) => by apply tac_pure_intro.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 3435e9b6e..3e86f4876 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -61,3 +61,13 @@ Definition bar {M} : uPred M := (∀ P, foo P)%I.
 
 Lemma demo_4 (M : cmraT) : True ⊢ @bar M.
 Proof. iIntros {P} "HP". done. Qed.
+
+Lemma demo_5 (M : cmraT) (x y : M) (P : uPred M) :
+  (∀ z, P → z ≡ y) ⊢ (P -★ (x,x) ≡ (y,x)).
+Proof.
+  iIntros "H1 H2".
+  iRewrite (uPred.eq_sym x x with "- !"). iApply uPred.eq_refl.
+  iRewrite -("H1" $! _ with "- !"); first done.
+  iApply uPred.eq_refl.
+Qed.
+
-- 
GitLab