Make it possible to introduce □ ⌜ φ ⌝ as a pure hypothesis.

theories/proofmode/class_instances.v

@@ -48,6 +48,9 @@ Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) :
   @IntoPure M (✓ a) (✓ a).
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
+Global Instance into_pure_always P φ : IntoPure P φ → IntoPure (□ P) φ.
+Proof. rewrite /IntoPure=> ->. by rewrite always_pure. Qed.
+
 Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∧ P2) (φ1 ∧ φ2).
 Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.

theories/tests/proofmode.v

@@ -80,6 +80,9 @@ Qed.
 Lemma test_iIntros_persistent P Q `{!PersistentP Q} : (P → Q → P ∗ Q)%I.
 Proof. iIntros "H1 H2". by iFrame. Qed.
 
+Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → (⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P)%I.
+Proof. iIntros (??) "H". auto. Qed.
+
 Lemma test_fast_iIntros P Q :
   (∀ x y z : nat,
     ⌜x = plus 0 x⌝ → ⌜y = 0⌝ → ⌜z = 0⌝ → P → □ Q → foo (x ≡ x))%I.