diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 1f47dcf15e308c48b3d5818a3c21622591c9e910..f7971a8a9657ee9bfe3224455eab039c70138f37 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -2,8 +2,8 @@ From iris.bi Require Export derived_connectives updates plainly.
 From iris.base_logic Require Export upred.
 Import uPred_primitive.
 
-(** BI instances for uPred, and re-stating the remaining primitive laws in terms
-of the BI interface.  This file does *not* unseal. *)
+(** BI instances for [uPred], and re-stating the remaining primitive laws in
+terms of the BI interface. This file does *not* unseal. *)
 
 Definition uPred_emp {M} : uPred M := uPred_pure True.
 
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 6d4df735c79f9720a229d974f30694c99aef22cb..39e86c98dc99919c2a32fe7828bd6a5ef1438177 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -339,7 +339,7 @@ Definition uPred_bupd_eq :
 (** Global uPred-specific Notation *)
 Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
 
-(** Promitive logical rules.
+(** Primitive logical rules.
     These are not directly usable later because they do not refer to the BI
     connectives. *)
 Module uPred_primitive.