Merge branch 'fix-wp-pure' into 'master'

Use [fill K] in tac_wp_pure

See merge request iris/iris!463

theories/heap_lang/proofmode.v

@@ -27,21 +27,21 @@ Tactic Notation "wp_expr_eval" tactic3(t) :=
   | _ => fail "wp_expr_eval: not a 'wp'"
   end.
 
-Lemma tac_wp_pure `{!heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
+Lemma tac_wp_pure `{!heapG Σ} Δ Δ' s E K e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
   MaybeIntoLaterNEnvs n Δ Δ' →
-  envs_entails Δ' (WP e2 @ s; E {{ Φ }}) →
-  envs_entails Δ (WP e1 @ s; E {{ Φ }}).
+  envs_entails Δ' (WP (fill K e2) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite HΔ' -lifting.wp_pure_step_later //.
 Qed.
-Lemma tac_twp_pure `{!heapG Σ} Δ s E e1 e2 φ n Φ :
+Lemma tac_twp_pure `{!heapG Σ} Δ s E K e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
-  envs_entails Δ (WP e2 @ s; E [{ Φ }]) →
-  envs_entails Δ (WP e1 @ s; E [{ Φ }]).
+  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 //.
 Qed.
@@ -84,7 +84,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
     let e := eval simpl in e in
     reshape_expr e ltac:(fun K e' =>
       unify e' efoc;
-      eapply (tac_wp_pure _ _ _ _ (fill K e'));
+      eapply (tac_wp_pure _ _ _ _ K e');
       [iSolveTC                       (* PureExec *)
       |try solve_vals_compare_safe    (* The pure condition for PureExec -- handles trivial goals, including [vals_compare_safe] *)
       |iSolveTC                       (* IntoLaters *)
@@ -95,7 +95,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
     let e := eval simpl in e in
     reshape_expr e ltac:(fun K e' =>
       unify e' efoc;
-      eapply (tac_twp_pure _ _ _ (fill K e'));
+      eapply (tac_twp_pure _ _ _ K e');
       [iSolveTC                       (* PureExec *)
       |try solve_vals_compare_safe    (* The pure condition for PureExec *)
       |wp_finish                      (* new goal *)