Merge branch 'ralf/pure-exec-fill' into 'master'

make pure_exec_fill not an instance any more

See merge request iris/iris!588

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.

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 :