From 35463c8da4c72066a83c43aba5d3e1a8718c85a5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 26 Nov 2020 20:06:17 +0100
Subject: [PATCH] make pure_exec_fill not an instance any more

---
 iris/program_logic/ectx_language.v | 7 ++++++-
 iris_heap_lang/proofmode.v         | 7 ++++++-
 2 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/iris/program_logic/ectx_language.v b/iris/program_logic/ectx_language.v
index df53a0185..09725d72c 100644
--- a/iris/program_logic/ectx_language.v
+++ b/iris/program_logic/ectx_language.v
@@ -298,7 +298,12 @@ Section ectx_language.
     - intros σ1 κ e2' σ2 efs ?%head_reducible_prim_step; eauto using head_reducible_no_obs_reducible.
   Qed.
 
-  Global Instance pure_exec_fill K φ n e1 e2 :
+  (** This is not an instance because HeapLang's [wp_pure] tactic already takes
+      care of handling the evaluation context.  So the instance is redundant.
+      If you are defining your own language and your [wp_pure] works
+      differently, you might want to specialize this lemma to your language and
+      register that as an instance. *)
+  Lemma pure_exec_fill K φ n e1 e2 :
     PureExec φ n e1 e2 →
     PureExec φ n (fill K e1) (fill K e2).
   Proof. apply: pure_exec_ctx. Qed.
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 46b122bfe..138042e2e 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -35,6 +35,8 @@ Lemma tac_wp_pure `{!heapG Σ} Δ Δ' s E K e1 e2 φ n Φ :
   envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
+  (* We want [pure_exec_fill] to be available to TC search locally. *)
+  pose proof @pure_exec_fill.
   rewrite HΔ' -lifting.wp_pure_step_later //.
 Qed.
 Lemma tac_twp_pure `{!heapG Σ} Δ s E K e1 e2 φ n Φ :
@@ -43,7 +45,10 @@ Lemma tac_twp_pure `{!heapG Σ} Δ s E K e1 e2 φ n Φ :
   envs_entails Δ (WP (fill K e2) @ s; E [{ Φ }]) →
   envs_entails Δ (WP (fill K e1) @ s; E [{ Φ }]).
 Proof.
-  rewrite envs_entails_eq=> ?? ->. rewrite -total_lifting.twp_pure_step //.
+  rewrite envs_entails_eq=> ?? ->.
+  (* We want [pure_exec_fill] to be available to TC search locally. *)
+  pose proof @pure_exec_fill.
+  rewrite -total_lifting.twp_pure_step //.
 Qed.
 
 Lemma tac_wp_value `{!heapG Σ} Δ s E Φ v :
-- 
GitLab