Merge branch 'robbert/bi_mono_pred' into 'master'

State `bi_mono_pred` using `□`/`-∗` instead of `<pers>`/`→`.

See merge request iris/iris!714

CHANGELOG.md

@@ -59,6 +59,7 @@ Coq 8.11 is no longer supported in this version of Iris.
     As a consequence, `make_laterable_elim` got weaker: elimination now requires
     an except-0 modality (`make_laterable P -∗ ◇ P`).
   - Add `iModIntro` support for `make_laterable`.
+* State `bi_mono_pred` using `□`/`-∗` instead of `<pers>`/`→`.
 
 **Changes in `proofmode`:**
 

iris/bi/lib/fixpoint.v

@@ -6,7 +6,7 @@ Import bi.
 (** Least and greatest fixpoint of a monotone function, defined entirely inside
     the logic.  *)
 Class BiMonoPred {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) := {
-  bi_mono_pred Φ Ψ : ⊢ <pers> (∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x;
+  bi_mono_pred Φ Ψ : □ (∀ x, Φ x -∗ Ψ x) -∗ ∀ x, F Φ x -∗ F Ψ x;
   bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
 }.
 Global Arguments bi_mono_pred {_ _ _ _} _ _.

iris/program_logic/total_adequacy.v

@@ -16,8 +16,8 @@ Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
               ∃ nt', ⌜κ = []⌝ ∗ state_interp σ2 (S ns) κs nt' ∗ twptp t2.
 
 Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
-  ⊢ <pers> (∀ t, twptp1 t -∗ twptp2 t) →
-    ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t.
+  □ (∀ t, twptp1 t -∗ twptp2 t) -∗
+  ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t.
 Proof.
   iIntros "#H"; iIntros (t) "Hwp". rewrite /twptp_pre.
   iIntros (t2 σ1 ns κ κs σ2 nt1) "Hstep Hσ".