From f02ecca36a0b8f6fc70194a2bc9107787f7e8972 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 13 May 2022 09:58:31 +0200
Subject: [PATCH] document what needs to be in pm_eval

---
 iris/proofmode/environments.v | 11 +++++------
 iris/proofmode/reduction.v    |  4 +++-
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index 941510915..cce61fffb 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -863,14 +863,13 @@ Proof.
   - rewrite /= IH (comm _ Q _) assoc. done.
 Qed.
 
-Lemma env_to_prop_and_pers_sound Γ :
-  □ env_to_prop_and Γ ⊣⊢ <affine> [∧] (env_map_pers Γ).
+Lemma env_to_prop_and_pers_sound Γ i P :
+  □ env_to_prop_and (Esnoc Γ i P) ⊣⊢ <affine> [∧] (env_map_pers (Esnoc Γ i P)).
 Proof.
-  destruct Γ as [|Γ i P]; simpl.
-  { rewrite /bi_intuitionistically persistent_persistently //. }
   revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
   - by rewrite right_id.
-  - rewrite /= IH (comm _ Q _) assoc. f_equiv.
-    rewrite persistently_and. done.
+  - rewrite /= IH. clear IH. f_equiv. simpl.
+    rewrite assoc. f_equiv.
+    rewrite persistently_and comm. done.
 Qed.
 End envs.
diff --git a/iris/proofmode/reduction.v b/iris/proofmode/reduction.v
index b70aef0a3..ff036d248 100644
--- a/iris/proofmode/reduction.v
+++ b/iris/proofmode/reduction.v
@@ -4,7 +4,9 @@ From iris.prelude Require Import options.
 
 (** Called by all tactics to perform computation to lookup items in the
     context.  We avoid reducing anything user-visible here to make sure we
-    do not reduce e.g. before unification happens in [iApply].*)
+    do not reduce e.g. before unification happens in [iApply].
+    This needs to contain all definitions used in the user-visible statements in
+    [coq_tactics], and their dependencies. *)
 Declare Reduction pm_eval := cbv [
   (* base *)
   base.negb base.beq
-- 
GitLab