From e3b9fa4381c02d7a95b9adad8eaf77a488f4df6f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 6 Dec 2019 20:28:58 +0100
Subject: [PATCH] Tweaks to comments in base_logic.

---
 theories/base_logic/bi.v    | 4 ++--
 theories/base_logic/upred.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 1f47dcf15..f7971a8a9 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 6d4df735c..39e86c98d 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.
-- 
GitLab