From c031da7d9ab6961c9232608ed4811eaca2cb5640 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 23 Jun 2016 13:56:32 +0200
Subject: [PATCH] Tactic iSimplifyEq that substitutes Leibniz equalities that
 are in the proof mode context.

---
 proofmode/tactics.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 21bd9cbab..eff7af382 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -34,6 +34,11 @@ Tactic Notation "iTypeOf" constr(H) tactic(tac):=
   | Some (?p,?P) => tac p P
   end.
 
+Ltac iMatchGoal tac :=
+  match goal with
+  | |- context[ environments.Esnoc _ ?x ?P ] => tac x P
+  end.
+
 (** * Start a proof *)
 Tactic Notation "iProof" :=
   lazymatch goal with
@@ -789,6 +794,10 @@ Tactic Notation "iRewrite" open_constr(t) "in" constr(H) :=
 Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
   iRewriteCore true t in H.
 
+Ltac iSimplifyEq := repeat (
+  iMatchGoal ltac:(fun H P => match P with (_ = _)%I => iDestruct H as %? end)
+  || simplify_eq/=).
+
 (* Make sure that by and done solve trivial things in proof mode *)
 Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
 Hint Extern 0 (of_envs _ ⊢ _) => iAssumption.
-- 
GitLab