Revert some proofmode changes

theories/logic/proofmode.v

@@ -11,21 +11,6 @@ From gpfsl.logic Require Export lifting.
 
 Require Import iris.prelude.options.
 
-Lemma tac_wp_expr_eval `{!noprolG Σ} Δ tid E Φ e e' :
-  (∀ (e'':=e'), e = e'') →
-  envs_entails Δ (WP e' @ tid; E {{ Φ }}) → envs_entails Δ (WP e @ tid; E {{ Φ }}).
-Proof. by intros ->. Qed.
-
-Tactic Notation "wp_expr_eval" tactic3(t) :=
-  iStartProof;
-  lazymatch goal with
-  | |- envs_entails _ (wp ?tid ?E ?e ?Q) =>
-    notypeclasses refine (tac_wp_expr_eval _ _ _ _ e _ _ _);
-      [let x := fresh in intros x; t; unfold x; notypeclasses refine eq_refl|]
-  | _ => fail "wp_expr_eval: not a 'wp'"
-  end.
-Ltac wp_expr_simpl := wp_expr_eval simpl.
-
 Lemma tac_wp_pure `{!noprolG Σ} K Δ Δ' tid E e1 e2 φ n Φ :
   (∀ 𝓥, PureExec φ n (e1 at 𝓥) (e2 at 𝓥)) →
   φ →
@@ -52,10 +37,9 @@ Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
 Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
 
 Ltac wp_finish :=
-  wp_expr_simpl;      (* simplify occurences of subst/fill *)
-  try wp_value_head;  (* in case we have reached a value, get rid of the WP *)
-  pm_prettify.        (* prettify ▷s caused by [MaybeIntoLaterNEnvs] and
-                         λs caused by wp_value *)
+  simpl_subst;        (* simplify occurences of subst/fill *)
+  try wp_value_head   (* in case we have reached a value, get rid of the WP *)
+  .
 
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;