From 0283ccbb535396dcee594a78282f7e453413c344 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 22 Dec 2016 10:51:27 +0100
Subject: [PATCH] fewer linebreaks in the core

---
 theories/base_logic/lib/core.v | 16 +++++-----------
 1 file changed, 5 insertions(+), 11 deletions(-)

diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index 910cbee7a..8d3663167 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -13,25 +13,19 @@ Section core.
   Context {M : ucmraT}.
   Implicit Types P Q : uPred M.
 
-  Lemma coreP_intro P :
-    P -∗ coreP P.
-  Proof.
-    iIntros "HP". iIntros (Q HQ HPQ). by iApply HPQ.
-  Qed.
+  Lemma coreP_intro P : P -∗ coreP P.
+  Proof. iIntros "HP". iIntros (Q HQ HPQ). by iApply HPQ. Qed.
 
-  Global Instance coreP_persistent P :
-    PersistentP (coreP P).
+  Global Instance coreP_persistent P : PersistentP (coreP P).
   Proof.
     iIntros "HCP". iApply always_forall. iIntros (Q).
     iApply always_forall. iIntros (HQ). iApply always_forall.
     iIntros (HPQ). iApply HQ. unshelve iApply ("HCP" $! Q). done.
   Qed.
 
-  Lemma corP_elim P :
-    PersistentP P → coreP P -∗ P.
+  Lemma corP_elim P : PersistentP P → coreP P -∗ P.
   Proof.
-    iIntros (?) "HCP". unshelve iApply ("HCP" $! P).
-    iIntros "P". done.
+    iIntros (?) "HCP". unshelve iApply ("HCP" $! P). iIntros "P". done.
   Qed.
 End core.
 
-- 
GitLab