diff --git a/algebra/ofe.v b/algebra/ofe.v
index 47d4fb8f8d4454af71bd83966a9e0e8fcfebace5..ec4c4d5e6cde18fa09f899b80fc36ec5a121ff44 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 dfb2bdf8340f9b07355e59b7dacddd20aa3cc08e..f2794751628968d14aa4a828f99fc4fa4adbde8c 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)))).