From 230b2a6beab7cccfc1de70139a35b1748dd62282 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 28 Nov 2016 17:04:03 +0100
Subject: [PATCH] Some nits.

---
 algebra/ofe.v          | 6 +++---
 base_logic/lib/boxes.v | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/algebra/ofe.v b/algebra/ofe.v
index 47d4fb8f8..ec4c4d5e6 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -342,11 +342,11 @@ Section unit.
   Definition unit_ofe_mixin : OfeMixin unit.
   Proof. by repeat split; try exists 0. Qed.
   Canonical Structure unitC : ofeT := OfeT unit unit_ofe_mixin.
-  
+
   Global Program Instance unit_cofe : Cofe unitC := { compl x := () }.
   Next Obligation. by repeat split; try exists 0. Qed.
-  
-Global Instance unit_discrete_cofe : Discrete unitC.
+
+  Global Instance unit_discrete_cofe : Discrete unitC.
   Proof. done. Qed.
 End unit.
 
diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v
index dfb2bdf83..f27947516 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -15,8 +15,8 @@ Section box_defs.
 
   Definition slice_name := gname.
 
-  Definition box_own_auth (γ : slice_name) (a : auth (option (excl bool)))
-    := own γ (a, (∅:option (agree (later (iPreProp Σ))))).
+  Definition box_own_auth (γ : slice_name) (a : auth (option (excl bool))) : iProp Σ :=
+    own γ (a, (∅:option (agree (later (iPreProp Σ))))).
 
   Definition box_own_prop (γ : slice_name) (P : iProp Σ) : iProp Σ :=
     own γ (∅:auth (option (excl bool)), Some (to_agree (Next (iProp_unfold P)))).
-- 
GitLab