Tweaks to comments in base_logic.

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.
 

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.