From 5bdc64619677c140748fe13e5339de7cb333a556 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 29 Sep 2020 12:38:45 +0200
Subject: [PATCH] Fix typos

---
 theories/algebra/monoid.v | 2 +-
 theories/algebra/ufrac.v  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/monoid.v b/theories/algebra/monoid.v
index 239d2d7fe..0c7a2e5f5 100644
--- a/theories/algebra/monoid.v
+++ b/theories/algebra/monoid.v
@@ -31,7 +31,7 @@ Proof. intros x. etrans; [apply monoid_comm|apply monoid_left_id]. Qed.
 
 (** The [Homomorphism] classes give rise to generic lemmas about big operators
 commuting with each other. We also consider a [WeakMonoidHomomorphism] which
-does not necesarrily commute with unit; an example is the [own] connective: we
+does not necessarily commute with unit; an example is the [own] connective: we
 only have `True ==∗ own γ ∅`, not `True ↔ own γ ∅`. *)
 Class WeakMonoidHomomorphism {M1 M2 : ofeT}
     (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) `{Monoid M1 o1, Monoid M2 o2}
diff --git a/theories/algebra/ufrac.v b/theories/algebra/ufrac.v
index ed629c467..91fc0e811 100644
--- a/theories/algebra/ufrac.v
+++ b/theories/algebra/ufrac.v
@@ -1,4 +1,4 @@
-(** This file provides a "bounded" version of the fractional camera whose
+(** This file provides an "unbounded" version of the fractional camera whose
 elements are in the interval (0,..) instead of (0,1]. *)
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
-- 
GitLab