fix typos in documentation: text

1 files changed, 9 insertions, 9 deletions

diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index bccafa8..9327a2f 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -6,7 +6,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 (*    The basic theory of paths over an eqType; this file is essentially a    *)
 (* complement to seq.v. Paths are non-empty sequences that obey a progression *)
 (* relation. They are passed around in three parts: the head and tail of the  *)
-(* sequence, and a proof of (boolean) predicate asserting the progression.    *)
+(* sequence, and a proof of a (boolean) predicate asserting the progression.  *)
 (* This "exploded" view is rarely embarrassing, as the first two parameters   *)
 (* are usually inferred from the type of the third; on the contrary, it saves *)
 (* the hassle of constantly constructing and destructing a dependent record.  *)
@@ -16,7 +16,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 (*   We allow duplicates; uniqueness, if desired (as is the case for several  *)
 (* geometric constructions), must be asserted separately. We do provide       *)
 (* shorthand, but only for cycles, because the equational properties of       *)
-(* "path" and "uniq" are unfortunately  incompatible (esp. wrt "cat").        *)
+(* "path" and "uniq" are unfortunately incompatible (esp. wrt "cat").         *)
 (*    We define notations for the common cases of function paths, where the   *)
 (* progress relation is actually a function. In detail:                       *)
 (*   path e x p == x :: p is an e-path [:: x_0; x_1; ... ; x_n], i.e., we     *)
@@ -26,7 +26,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 (*                 the form [:: f x; f (f x); ...]. This is just a notation   *)
 (*                 for path (frel f) x p.                                     *)
 (*   sorted e s == s is an e-sorted sequence: either s = [::], or s = x :: p  *)
-(*                 is an e-path (this is oten used with e = leq or ltn).      *)
+(*                 is an e-path (this is often used with e = leq or ltn).     *)
 (*    cycle e c == c is an e-cycle: either c = [::], or c = x :: p with       *)
 (*                 x :: (rcons p x) an e-path.                                *)
 (*   fcycle f c == c is an f-cycle, for a function f.                         *)
@@ -47,9 +47,9 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 (*                 c (viewed as a cycle), or x if x \notin c.                 *)
 (*     prev c x == the predecessor of the first occurrence of x in the        *)
 (*                 sequence c (viewed as a cycle), or x if x \notin c.        *)
-(*    arc c x y == the sub-arc of the sequece c (viewed as a cycle) starting  *)
+(*    arc c x y == the sub-arc of the sequence c (viewed as a cycle) starting *)
 (*                 at the first occurrence of x in c, and ending just before  *)
-(*                 the next ocurrence of y (in cycle order); arc c x y        *)
+(*                 the next occurrence of y (in cycle order); arc c x y       *)
 (*                 returns an unspecified sub-arc of c if x and y do not both *)
 (*                 occur in c.                                                *)
 (*  ucycle e c <-> ucycleb e c (ucycle e c is a Coercion target of type Prop) *)
@@ -73,12 +73,12 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 (*    of splitP will also simultaneously replace take (index x p) with p1 and *)
 (*    drop (index x p).+1 p with p2.                                          *)
 (*  - splitPl applies when x \in x0 :: p; it replaces p with p1 ++ p2 and     *)
-(*    simulaneously generates an equation x = last x0 p.                      *)
+(*    simultaneously generates an equation x = last x0 p.                     *)
 (*  - splitPr applies when x \in p; it replaces p with (p1 ++ x :: p2), so x  *)
 (*    appears explicitly at the start of the right part.                      *)
 (* The parts p1 and p2 are computed using index/take/drop in all cases, but   *)
-(* only splitP attemps to subsitute the explicit values. The substitution of  *)
-(* p can be deferred using the dependent equation generation feature of       *)
+(* only splitP attempts to substitute the explicit values. The substitution   *)
+(* of p can be deferred using the dependent equation generation feature of    *)
 (* ssreflect, e.g.: case/splitPr def_p: {1}p / x_in_p => [p1 p2] generates    *)
 (* the equation p = p1 ++ p2 instead of performing the substitution outright. *)
 (*   Similarly, eliminating the loop removal lemma shortenP simultaneously    *)
@@ -86,7 +86,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 (* last x p'.                                                                 *)
 (*   Note that although all "path" functions actually operate on the          *)
 (* underlying sequence, we provide a series of lemmas that define their       *)
-(* interaction with thepath and cycle predicates, e.g., the cat_path equation *)
+(* interaction with the path and cycle predicates, e.g., the cat_path equation*)
 (* can be used to split the path predicate after splitting the underlying     *)
 (* sequence.                                                                  *)
 (******************************************************************************)