diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 753eec0ac5f730ab00c9d05e742a4d8a7320b062..3a8790f91e3af0824eb557062ae1b87af4b09513 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -30,13 +30,16 @@ Proof. by rewrite /IntoPure discrete_valid. Qed.
 
 (* FromPure *)
 Global Instance from_pure_pure φ : @FromPure M (■ φ) φ.
-Proof. intros ?. by apply pure_intro. Qed.
+Proof. done. Qed.
 Global Instance from_pure_eq {A : cofeT} (a b : A) : @FromPure M (a ≡ b) (a ≡ b).
-Proof. intros ->. apply eq_refl. Qed.
+Proof. rewrite /FromPure. eapply pure_elim; [done|]=> ->. apply eq_refl'. Qed.
 Global Instance from_pure_valid {A : cmraT} (a : A) : @FromPure M (✓ a) (✓ a).
-Proof. intros ?. by apply valid_intro. Qed.
+Proof.
+  rewrite /FromPure. eapply pure_elim; [done|]=> ?.
+  rewrite -valid_intro //. auto with I.
+Qed.
 Global Instance from_pure_rvs P φ : FromPure P φ → FromPure (|=r=> P) φ.
-Proof. intros ??. by rewrite -rvs_intro (from_pure P). Qed.
+Proof. rewrite /FromPure=> ->. apply rvs_intro. Qed.
 
 (* IntoPersistentP *)
 Global Instance into_persistentP_always_trans P Q :
diff --git a/proofmode/classes.v b/proofmode/classes.v
index 83c1f2e7c22378f98eca6118b94e7bb04c166042..ac65c81e3c600675c27a64f1724a6670a80eeb4f 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -11,7 +11,7 @@ Global Arguments from_assumption _ _ _ {_}.
 Class IntoPure (P : uPred M) (φ : Prop) := into_pure : P ⊢ ■ φ.
 Global Arguments into_pure : clear implicits.
 
-Class FromPure (P : uPred M) (φ : Prop) := from_pure : φ → True ⊢ P.
+Class FromPure (P : uPred M) (φ : Prop) := from_pure : ■ φ ⊢ P.
 Global Arguments from_pure : clear implicits.
 
 Class IntoPersistentP (P Q : uPred M) := into_persistentP : P ⊢ □ Q.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 0917c2769e0a226e24ef15b77f57714312f8d3ab..0c73bba5a7242d133a7346d6045b31adcf1efd9e 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -318,7 +318,7 @@ Proof. by rewrite -(False_elim Q). Qed.
 
 (** * Pure *)
 Lemma tac_pure_intro Δ Q (φ : Prop) : FromPure Q φ → φ → Δ ⊢ Q.
-Proof. intros ??. rewrite -(from_pure Q) //. apply True_intro. Qed.
+Proof. intros ??. rewrite -(from_pure Q). by apply pure_intro. Qed.
 
 Lemma tac_pure Δ Δ' i p P φ Q :
   envs_lookup_delete i Δ = Some (p, P, Δ') → IntoPure P φ →
@@ -495,7 +495,8 @@ Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
   φ → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl.
-  by rewrite right_id (into_wand R) -(from_pure P1) // wand_True wand_elim_r.
+  rewrite right_id (into_wand R) -(from_pure P1) pure_equiv //.
+  by rewrite wand_True wand_elim_r.
 Qed.
 
 Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index e3641da1c84232d2986ba90c6d1dd88db33e459c..ecdc794a5e363a601bcd071abc5292d00f6ecdb1 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -8,7 +8,7 @@ Context `{irisG Λ Σ}.
 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.
+Proof. rewrite /FromPure. intros <-. apply pvs_intro. Qed.
 
 Global Instance from_assumption_pvs E p P Q :
   FromAssumption p P (|=r=> Q) → FromAssumption p P (|={E}=> Q)%I.