From b0eb3ed9e9c4277d138626a5be7e5a954c3cfc35 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 8 Nov 2021 10:34:28 -0500
Subject: [PATCH] formatting and nits

---
 iris/base_logic/bi.v   | 2 +-
 iris/bi/derived_laws.v | 3 +--
 iris/bi/interface.v    | 2 +-
 iris/bi/lib/core.v     | 3 ++-
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index cf20a664c..f803dbd10 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -53,7 +53,7 @@ Proof.
   - exact: persistently_idemp_2.
   - (* emp ⊢ <pers> emp (ADMISSIBLE) *)
     trans (uPred_forall (M:=M) (λ _ : False, uPred_persistently uPred_emp)).
-    + apply forall_intro=>[[]].
+    + apply forall_intro=>-[].
     + etrans; first exact: persistently_forall_2.
       apply persistently_mono. exact: pure_intro.
   - (* ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q) (ADMISSIBLE) *)
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index 9d29b036c..c7aa96c06 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -862,8 +862,7 @@ Lemma persistently_and P Q : <pers> (P ∧ Q) ⊣⊢ <pers> P ∧ <pers> Q.
 Proof. apply (anti_symm _); by auto using persistently_and_2. Qed.
 Lemma persistently_or P Q : <pers> (P ∨ Q) ⊣⊢ <pers> P ∨ <pers> Q.
 Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
-Lemma persistently_impl P Q :
-  <pers> (P → Q) ⊢ <pers> P → <pers> Q.
+Lemma persistently_impl P Q : <pers> (P → Q) ⊢ <pers> P → <pers> Q.
 Proof.
   apply impl_intro_l; rewrite -persistently_and.
   apply persistently_mono, impl_elim with P; auto.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index ef82d1380..3317c511c 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -107,7 +107,7 @@ Section bi_mixin.
     The null-ary case, [persistently_True : True ⊢ <pers> True], is derivable from the
     other laws. *)
     bi_mixin_persistently_and_2 (P Q : PROP) :
-      ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q);
+      (<pers> P) ∧ (<pers> Q) ⊢ <pers> (P ∧ Q);
     bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
       <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a);
 
diff --git a/iris/bi/lib/core.v b/iris/bi/lib/core.v
index 9b4c499ab..0bc59a54f 100644
--- a/iris/bi/lib/core.v
+++ b/iris/bi/lib/core.v
@@ -26,7 +26,8 @@ Section core.
     by iApply "HPQ".
   Qed.
 
-  Global Instance coreP_persistent `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} P :
+  Global Instance coreP_persistent
+      `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} P :
     Persistent (coreP P).
   Proof.
     rewrite /coreP /Persistent. iIntros "HC" (Q).
-- 
GitLab