From df17e4c2e890b4a1f5d9ae4358ff254ccb52c1e9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 31 Dec 2017 17:53:41 +0100
Subject: [PATCH] `iSimpl` tactic that `simpl`s the proofmode goal.

---
 theories/proofmode/coq_tactics.v | 5 +++++
 theories/proofmode/tactics.v     | 7 +++++++
 2 files changed, 12 insertions(+)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index a6729546d..299d9b5cd 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -413,6 +413,11 @@ Proof.
 Qed.
 
 (** * Basic rules *)
+Lemma tac_eval Δ Q Q' :
+  Q = Q' →
+  envs_entails Δ Q' → envs_entails Δ Q.
+Proof. by intros ->. Qed.
+
 Lemma tac_assumption Δ i p P Q :
   envs_lookup i Δ = Some (p,P) → FromAssumption p P Q →
   envs_entails Δ Q.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 315d0dccc..e470ea48c 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -80,6 +80,13 @@ Ltac iStartProof :=
                |apply tac_adequate]
   end.
 
+(** * Simplification *)
+Tactic Notation "iEval" tactic(t) :=
+  try iStartProof;
+  try (eapply tac_eval; [t; reflexivity|]).
+
+Tactic Notation "iSimpl" := iEval simpl.
+
 (** * Context manipulation *)
 Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
   eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
-- 
GitLab