diff --git a/proofmode/classes.v b/proofmode/classes.v
index c14e4b886dd7574b6d15b9e10d743f894a455e4e..b30f4311c5ca4cc0840a05f2bbad5867ffef12a5 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -17,15 +17,24 @@ Global Instance from_assumption_always_r P Q :
   FromAssumption true P Q → FromAssumption true P (□ Q).
 Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
 
-Class IsPure (P : uPred M) (φ : Prop) := is_pure : P ⊣⊢ ■ φ.
-Global Arguments is_pure : clear implicits.
-Global Instance is_pure_pure φ : IsPure (■ φ) φ.
+Class IntoPure (P : uPred M) (φ : Prop) := into_pure : P ⊢ ■ φ.
+Global Arguments into_pure : clear implicits.
+Global Instance into_pure_pure φ : IntoPure (■ φ) φ.
 Proof. done. Qed.
-Global Instance is_pure_eq {A : cofeT} (a b : A) :
-  Timeless a → IsPure (a ≡ b) (a ≡ b).
-Proof. intros; red. by rewrite timeless_eq. Qed.
-Global Instance is_pure_valid `{CMRADiscrete A} (a : A) : IsPure (✓ a) (✓ a).
-Proof. intros; red. by rewrite discrete_valid. Qed.
+Global Instance into_pure_eq {A : cofeT} (a b : A) :
+  Timeless a → IntoPure (a ≡ b) (a ≡ b).
+Proof. intros. by rewrite /IntoPure timeless_eq. Qed.
+Global Instance into_pure_valid `{CMRADiscrete A} (a : A) : IntoPure (✓ a) (✓ a).
+Proof. by rewrite /IntoPure discrete_valid. Qed.
+
+Class FromPure (P : uPred M) (φ : Prop) := from_pure : φ → True ⊢ P.
+Global Arguments from_pure : clear implicits.
+Global Instance from_pure_pure φ : FromPure (■ φ) φ.
+Proof. intros ?. by apply pure_intro. Qed.
+Global Instance from_pure_eq {A : cofeT} (a b : A) : FromPure (a ≡ b) (a ≡ b).
+Proof. intros ->. apply eq_refl. Qed.
+Global Instance from_pure_valid {A : cmraT} (a : A) : FromPure (✓ a) (✓ a).
+Proof. intros ?. by apply valid_intro. Qed.
 
 Class IntoPersistentP (P Q : uPred M) := into_persistentP : P ⊢ □ Q.
 Global Arguments into_persistentP : clear implicits.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 12144b1d348fdc07e036acecc73d96bed113c92d..e35620930014910c450599f4688884f1663317ff 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -316,15 +316,15 @@ Lemma tac_ex_falso Δ Q : (Δ ⊢ False) → Δ ⊢ Q.
 Proof. by rewrite -(False_elim Q). Qed.
 
 (** * Pure *)
-Lemma tac_pure_intro Δ Q (φ : Prop) : IsPure Q φ → φ → Δ ⊢ Q.
-Proof. intros ->. apply pure_intro. Qed.
+Lemma tac_pure_intro Δ Q (φ : Prop) : FromPure Q φ → φ → Δ ⊢ Q.
+Proof. intros ??. rewrite -(from_pure Q) //. apply True_intro. Qed.
 
 Lemma tac_pure Δ Δ' i p P φ Q :
-  envs_lookup_delete i Δ = Some (p, P, Δ') → IsPure P φ →
+  envs_lookup_delete i Δ = Some (p, P, Δ') → IntoPure P φ →
   (φ → Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
-  rewrite (is_pure P); by apply pure_elim_sep_l.
+  rewrite (into_pure P); by apply pure_elim_sep_l.
 Qed.
 
 Lemma tac_pure_revert Δ φ Q : (Δ ⊢ ■ φ → Q) → (φ → Δ ⊢ Q).
@@ -405,9 +405,9 @@ Proof.
   intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
   by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
 Qed.
-Lemma tac_impl_intro_pure Δ P φ Q : IsPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P → Q.
+Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P → Q.
 Proof.
-  intros. by apply impl_intro_l; rewrite (is_pure P); apply pure_elim_l.
+  intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
 Qed.
 
 Lemma tac_wand_intro Δ Δ' i P Q :
@@ -423,9 +423,9 @@ Proof.
   intros. rewrite envs_app_sound //; simpl.
   rewrite right_id. by apply wand_mono.
 Qed.
-Lemma tac_wand_intro_pure Δ P φ Q : IsPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P -★ Q.
+Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P -★ Q.
 Proof.
-  intros. by apply wand_intro_l; rewrite (is_pure P); apply pure_elim_sep_l.
+  intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l.
 Qed.
 
 (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
@@ -476,12 +476,12 @@ Qed.
 
 Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
   envs_lookup j Δ = Some (q, R) →
-  IntoWand R P1 P2 → IsPure P1 φ →
+  IntoWand R P1 P2 → FromPure P1 φ →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
   φ → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl.
-  by rewrite right_id (into_wand R) (is_pure P1) pure_equiv // wand_True wand_elim_r.
+  by rewrite right_id (into_wand R) -(from_pure P1) // wand_True wand_elim_r.
 Qed.
 
 Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 86afa3f6b9fb6156a51c91eb8df1573bbe389ba2..013403208e937224eedac6686d31d9359d961f67 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -7,6 +7,8 @@ Section pvs.
 Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q : iProp Λ Σ.
 
+Global Instance from_pure_pvs E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
+Proof. intros ??. by rewrite -pvs_intro (from_pure P). Qed.
 Global Instance from_assumption_pvs E p P Q :
   FromAssumption p P Q → FromAssumption p P (|={E}=> Q)%I.
 Proof. rewrite /FromAssumption=>->. apply pvs_intro. Qed.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 1724a373082c2e5d3f47c5ba7acb7da993cd197c..72dacaf195a30b8384ee4c076af6fcd10d089a5a 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -112,13 +112,13 @@ Local Tactic Notation "iPersistent" constr(H) :=
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
   eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
     [env_cbv; reflexivity || fail "iPure:" H "not found"
-    |let P := match goal with |- IsPure ?P _ => P end in
+    |let P := match goal with |- IntoPure ?P _ => P end in
      apply _ || fail "iPure:" H ":" P "not pure"
     |intros pat].
 
 Tactic Notation "iPureIntro" :=
   eapply tac_pure_intro;
-    [let P := match goal with |- IsPure ?P _ => P end in
+    [let P := match goal with |- FromPure ?P _ => P end in
      apply _ || fail "iPureIntro:" P "not pure"|].
 
 (** * Specialize *)
@@ -184,7 +184,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
        eapply tac_specialize_pure with _ H1 _ _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |let Q := match goal with |- IsPure ?Q _ => Q end in
+         |let Q := match goal with |- FromPure ?Q _ => Q end in
           apply _ || fail "iSpecialize:" Q "not pure"
          |env_cbv; reflexivity
          |(*goal*)
@@ -505,11 +505,11 @@ Tactic Notation "iNext":=
 Local Tactic Notation "iIntro" "{" simple_intropattern(x) "}" := first
   [ (* (∀ _, _) *) apply tac_forall_intro; intros x
   | (* (?P → _) *) eapply tac_impl_intro_pure;
-     [let P := match goal with |- IsPure ?P _ => P end in
+     [let P := match goal with |- IntoPure ?P _ => P end in
       apply _ || fail "iIntro:" P "not pure"
      |intros x]
   | (* (?P -★ _) *) eapply tac_wand_intro_pure;
-     [let P := match goal with |- IsPure ?P _ => P end in
+     [let P := match goal with |- IntoPure ?P _ => P end in
       apply _ || fail "iIntro:" P "not pure"
      |intros x]
   |intros x].
diff --git a/tests/one_shot.v b/tests/one_shot.v
index e1b70e06a213b1e73f2abaebb6d05502442d5c5a..6f6e0c53fb4d5921d6082d3d11fe6e5b7f7d091d 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -71,7 +71,7 @@ Proof.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
     wp_let. iPvsIntro. iIntros "!". wp_seq.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as {m} "[% Hγ']"; subst.
-    { wp_match. by iPvsIntro. }
+    { by wp_match. }
     wp_match. wp_focus (! _)%E.
     iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as {m'} "[Hl Hγ]".
     { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". }
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 24edb16fcc2af18a56fd0b6b817f4243e06c26e5..6b7697cb89f6f6832a34fbc803dbe4484b9e9130 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import tactics notation.
 From iris.proofmode Require Import pviewshifts invariants.
 
 Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
@@ -103,6 +103,6 @@ Section iris.
     iApply ("H" with "[#] HP |==>[HQ] |==>").
     - done.
     - by iApply inv_alloc.
-    - by iPvsIntro.
+    - done.
   Qed.
 End iris.