final tweaks

iris_heap_lang/primitive_laws.v

@@ -170,18 +170,6 @@ Proof.
   iIntros "_". iPureIntro. rewrite /num_laters_per_step /=. lia.
 Qed.
 
-(** This just re-exports the lifting lemma when one wants to generate a single
-credit during a pure step. *)
-Lemma wp_pure_step_credit s E e1 e2 ϕ Φ :
-  PureExec ϕ 1 e1 e2 →
-  ϕ →
-  ▷ (£ 1 -∗ WP e2 @ s; E {{ Φ }}) -∗
-  WP e1 @ s; E {{ Φ }}.
-Proof.
-  iIntros (Hexec Hphi) "Hwp".
-  iApply wp_pure_step_later; done.
-Qed.
-
 (** Recursive functions: we do not use this lemmas as it is easier to use Löb
 induction directly, but this demonstrates that we can state the expected
 reasoning principle for recursive functions, without any visible ▷. *)

iris_heap_lang/proofmode.v

@@ -57,16 +57,16 @@ Lemma tac_wp_pure_credit `{!heapGS_gen hlc Σ} Δ Δ' s E j K e1 e2 ϕ Φ :
   PureExec ϕ 1 e1 e2 →
   ϕ →
   MaybeIntoLaterNEnvs 1 Δ Δ' →
-  (match envs_app false (Esnoc Enil j (£ 1)) Δ' with
-    | Some Δ'' =>
-       envs_entails Δ'' (WP fill K e2 @ s; E {{ Φ }})
-    | None => False
-    end) →
+  match envs_app false (Esnoc Enil j (£ 1)) Δ' with
+  | Some Δ'' =>
+     envs_entails Δ'' (WP fill K e2 @ s; E {{ Φ }})
+  | None => False
+  end →
   envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_unseal=> ??? HΔ.
   pose proof @pure_exec_fill.
-  rewrite -wp_pure_step_credit; last done.
+  rewrite -lifting.wp_pure_step_later; last done.
   rewrite into_laterN_env_sound /=. apply later_mono.
   destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ].
   rewrite envs_app_sound //; simpl.
@@ -161,7 +161,7 @@ Tactic Notation "wp_pure" open_constr(efoc) "credit:" constr(H) :=
   let Htmp := iFresh in
   let finish _ :=
     pm_reduce;
-    (iDestructHyp Htmp as H || fail 2 "wp_pure: " H " is not fresh");
+    (iDestructHyp Htmp as H || fail 2 "wp_pure:" H "is not fresh");
     wp_finish
     in
   lazymatch goal with

tests/heap_lang.ref

@@ -193,7 +193,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 "test_wp_pure_credit_fail"
      : string
 The command has indeed failed with message:
-Tactic failure: wp_pure:  "Hcred"  is not fresh.
+Tactic failure: wp_pure: "Hcred" is not fresh.
 1 goal
   
   Σ : gFunctors