Fixing typos - Part 3

3 files changed, 3 insertions, 3 deletions

diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index d000b75bf4..e5b2e22dc1 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -208,7 +208,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
   unfold eqb; intros; destruct (eq_dec x y); elim_comp; auto.
   Qed.
 
-(* Specialization of resuts about lists modulo. *)
+(* Specialization of results about lists modulo. *)
 
 Section ForNotations.
 
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 182b781fe1..354c1eb9b0 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -431,7 +431,7 @@ Proof.
 apply eq_true_iff_eq. now rewrite negb_true_iff, ltb_lt, leb_gt.
 Qed.
 
-(** Relation bewteen [compare] and the boolean comparisons *)
+(** Relation between [compare] and the boolean comparisons *)
 
 Lemma eqb_compare x y :
  (x =? y) = match compare x y with Eq => true | _ => false end.
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v
index ebd8ee8fc2..80925ff058 100644
--- a/theories/Structures/OrdersTac.v
+++ b/theories/Structures/OrdersTac.v
@@ -51,7 +51,7 @@ Local Infix "+" := trans_ord.
 
    This used to be provided here via a [TotalOrder], but
    for technical reasons related to extraction, we now ask
-   for two sperate parts: relations in a [EqLtLe] + properties in
+   for two separate parts: relations in a [EqLtLe] + properties in
    [IsTotalOrder]. Note that [TotalOrder = EqLtLe <+ IsTotalOrder]
 *)