aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mathcomp/algebra/matrix.v8
-rw-r--r--mathcomp/algebra/poly.v2
-rw-r--r--mathcomp/character/integral_char.v2
-rw-r--r--mathcomp/character/mxabelem.v2
-rw-r--r--mathcomp/field/algnum.v2
-rw-r--r--mathcomp/ssreflect/bigop.v6
-rw-r--r--mathcomp/ssreflect/binomial.v2
-rw-r--r--mathcomp/ssreflect/eqtype.v6
-rw-r--r--mathcomp/ssreflect/finfun.v4
-rw-r--r--mathcomp/ssreflect/fingraph.v2
-rw-r--r--mathcomp/ssreflect/finset.v10
-rw-r--r--mathcomp/ssreflect/fintype.v2
-rw-r--r--mathcomp/ssreflect/generic_quotient.v6
-rw-r--r--mathcomp/ssreflect/order.v12
-rw-r--r--mathcomp/ssreflect/path.v18
-rw-r--r--mathcomp/ssreflect/prime.v2
-rw-r--r--mathcomp/ssreflect/ssrnat.v8
-rw-r--r--mathcomp/ssreflect/ssrnotations.v2
-rw-r--r--mathcomp/ssreflect/tuple.v2
19 files changed, 49 insertions, 49 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 0725885..dfdaf8b 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -100,7 +100,7 @@ From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg.
(* \adj A == the adjugate matrix of A (\adj A i j = cofactor j i A). *)
(* A \in unitmx == A is invertible (R must be a comUnitRingType). *)
(* invmx A == the inverse matrix of A if A \in unitmx A, otherwise A. *)
-(* The following operations provide a correspondance between linear functions *)
+(* The following operations provide a correspondence between linear functions *)
(* and matrices: *)
(* lin1_mx f == the m x n matrix that emulates via right product *)
(* a (linear) function f : 'rV_m -> 'rV_n on ROW VECTORS *)
@@ -1837,7 +1837,7 @@ Lemma mulmx_block m1 m2 n1 n2 p1 p2 (Aul : 'M_(m1, n1)) (Aur : 'M_(m1, n2))
(Adl *m Bul + Adr *m Bdl) (Adl *m Bur + Adr *m Bdr).
Proof. by rewrite mul_col_mx !mul_row_block. Qed.
-(* Correspondance between matrices and linear function on row vectors. *)
+(* Correspondence between matrices and linear function on row vectors. *)
Section LinRowVector.
Variables m n : nat.
@@ -1856,7 +1856,7 @@ Qed.
End LinRowVector.
-(* Correspondance between matrices and linear function on matrices. *)
+(* Correspondence between matrices and linear function on matrices. *)
Section LinMatrix.
Variables m1 n1 m2 n2 : nat.
@@ -1959,7 +1959,7 @@ by congr (_ + _); apply: eq_bigr => i _; rewrite (block_mxEul, block_mxEdr).
Qed.
(* The matrix ring structure requires a strutural condition (dimension of the *)
-(* form n.+1) to statisfy the nontriviality condition we have imposed. *)
+(* form n.+1) to satisfy the nontriviality condition we have imposed. *)
Section MatrixRing.
Variable n' : nat.
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index e25d7c0..d21e690 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -10,7 +10,7 @@ From mathcomp Require Import fintype bigop div ssralg countalg binomial tuple.
(* *)
(* {poly R} == the type of polynomials with coefficients of type R, *)
(* represented as lists with a non zero last element *)
-(* (big endian representation); the coeficient type R *)
+(* (big endian representation); the coefficient type R *)
(* must have a canonical ringType structure cR. In fact *)
(* {poly R} denotes the concrete type polynomial cR; R *)
(* is just a phantom argument that lets type inference *)
diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v
index 7e470b2..2b886a6 100644
--- a/mathcomp/character/integral_char.v
+++ b/mathcomp/character/integral_char.v
@@ -83,7 +83,7 @@ Qed.
Section GenericClassSums.
(* This is Isaacs, Theorem (2.4), generalized to an arbitrary field, and with *)
-(* the combinatorial definition of the coeficients exposed. *)
+(* the combinatorial definition of the coefficients exposed. *)
(* This part could move to mxrepresentation.*)
Variable (gT : finGroupType) (G : {group gT}) (F : fieldType).
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v
index 1c3fe0b..92470d9 100644
--- a/mathcomp/character/mxabelem.v
+++ b/mathcomp/character/mxabelem.v
@@ -11,7 +11,7 @@ From mathcomp Require Import mxalgebra mxrepresentation.
(******************************************************************************)
(* This file completes the theory developed in mxrepresentation.v with the *)
(* construction and properties of linear representations over finite fields, *)
-(* and in particular the correspondance between internal action on a (normal) *)
+(* and in particular the correspondence between internal action on a (normal) *)
(* elementary abelian p-subgroup and a linear representation on an Fp-module. *)
(* We provide the following next constructions for a finite field F: *)
(* 'Zm%act == the action of {unit F} on 'M[F]_(m, n). *)
diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v
index 15d1d61..ad02f44 100644
--- a/mathcomp/field/algnum.v
+++ b/mathcomp/field/algnum.v
@@ -17,7 +17,7 @@ From mathcomp Require Import cyclotomic.
(* x \in Cint_span X <=> x is a Z-linear combination of elements of *)
(* X : seq algC. *)
(* x \in Aint <=> x : algC is an algebraic integer, i.e., the (monic) *)
-(* polynomial of x over Q has integer coeficients. *)
+(* polynomial of x over Q has integer coefficients. *)
(* (e %| a)%A <=> e divides a with respect to algebraic integers, *)
(* (e %| a)%Ax i.e., a is in the algebraic integer ideal generated *)
(* by e. This is is notation for a \in dvdA e, where *)
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 6d18825..698f2e7 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -5,12 +5,12 @@ From mathcomp Require Import div fintype tuple finfun.
(******************************************************************************)
(* This file provides a generic definition for iterating an operator over a *)
-(* set of indices (bigop); this big operator is parametrized by the return *)
+(* set of indices (bigop); this big operator is parameterized by the return *)
(* type (R), the type of indices (I), the operator (op), the default value on *)
(* empty lists (idx), the range of indices (r), the filter applied on this *)
(* range (P) and the expression we are iterating (F). The definition is not *)
(* to be used directly, but via the wide range of notations provided and *)
-(* and which support a natural use of big operators. *)
+(* which support a natural use of big operators. *)
(* To improve performance of the Coq typechecker on large expressions, the *)
(* bigop constant is OPAQUE. It can however be unlocked to reveal the *)
(* transparent constant reducebig, to let Coq expand summation on an explicit *)
@@ -27,7 +27,7 @@ From mathcomp Require Import div fintype tuple finfun.
(* 2. Results depending on the properties of the operator: *)
(* We distinguish: monoid laws (op is associative, idx is an identity *)
(* element), abelian monoid laws (op is also commutative), and laws with *)
-(* a distributive operation (semi-rings). Examples of such results are *)
+(* a distributive operation (semirings). Examples of such results are *)
(* splitting, permuting, and exchanging bigops. *)
(* A special section is dedicated to big operators on natural numbers. *)
(******************************************************************************)
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index 3a484a1..2af7953 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -5,7 +5,7 @@ From mathcomp Require Import div fintype tuple finfun bigop prime finset.
(******************************************************************************)
(* This files contains the definition of: *)
-(* 'C(n, m) == the binomial coeficient n choose m. *)
+(* 'C(n, m) == the binomial coefficient n choose m. *)
(* n ^_ m == the falling (or lower) factorial of n with m terms, i.e., *)
(* the product n * (n - 1) * ... * (n - m + 1). *)
(* Note that n ^_ m = 0 if m > n, and 'C(n, m) = n ^_ m %/ m/!. *)
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index f5d95e8..296f85e 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -38,7 +38,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool.
(* x != y :> T <=> x and y compare unequal at type T. *)
(* x =P y :: a proof of reflect (x = y) (x == y); x =P y coerces *)
(* to x == y -> x = y. *)
-(* eq_op == the boolean relation behing the == notation. *)
+(* eq_op == the boolean relation behind the == notation. *)
(* pred1 a == the singleton predicate [pred x | x == a]. *)
(* pred2, pred3, pred4 == pair, triple, quad predicates. *)
(* predC1 a == [pred x | x != a]. *)
@@ -73,7 +73,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool.
(* insub x = Some u with val u = x if P x, *)
(* None if ~~ P x *)
(* The insubP lemma encapsulates this dichotomy. *)
-(* P should be infered from the expected return type. *)
+(* P should be inferred from the expected return type. *)
(* innew x == total (non-option) variant of insub when P = predT. *)
(* {? x | P} == option {x | P} (syntax for casting insub x). *)
(* insubd u0 x == the generic projection with default value u0. *)
@@ -92,7 +92,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool.
(* [subType for S_val by Srect], [newType for S_val by Srect] *)
(* variants of the above where the eliminator is explicitly provided. *)
(* Here S no longer needs to be syntactically identical to {x | P x} or *)
-(* wrapped T, but it must have a derived constructor S_Sub statisfying an *)
+(* wrapped T, but it must have a derived constructor S_Sub satisfying an *)
(* eliminator Srect identical to the one the Coq Inductive command would *)
(* have generated, and S_val (S_Sub x Px) (resp. S_val (S_sub x) for the *)
(* newType form) must be convertible to x. *)
diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v
index 749f5e2..0218f6a 100644
--- a/mathcomp/ssreflect/finfun.v
+++ b/mathcomp/ssreflect/finfun.v
@@ -39,7 +39,7 @@ From mathcomp Require Import fintype tuple.
(* limitations referred to above. *)
(* ffun0 aT0 == the trivial finfun, from a proof aT0 that #|aT| = 0. *)
(* f \in family F == f belongs to the family F (f x \in F x for all x) *)
-(* There are addidional operations for non-dependent finite functions, *)
+(* There are additional operations for non-dependent finite functions, *)
(* i.e., f in {ffun aT -> rT}. *)
(* [ffun x => E] := finfun (fun x => E). *)
(* The type of E must not depend on x; this restriction *)
@@ -155,7 +155,7 @@ Proof. by fix IHt 2 => n [st]; apply/Kstep=> i; apply: IHt. Defined.
Set Elimination Schemes.
(* End example. *) *)
-(* The correspondance between finfun_of and CiC dependent functions. *)
+(* The correspondence between finfun_of and CiC dependent functions. *)
Section DepPlainTheory.
Variables (aT : finType) (rT : aT -> Type).
Notation fT := {ffun finPi aT rT}.
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index afd43df..09ca95f 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -776,7 +776,7 @@ Qed.
(* has to apply it to the natural numbers corresponding to the line, e.g. *)
(* `orbitPcycle 0 2 : fcycle f (orbit x) <-> exists k, iter k.+1 f x = x`. *)
(* examples of this are in order_id_cycle and fconnnect_f. *)
-(* One may also use lemma all_iffLR to get a one sided impliciation, as in *)
+(* One may also use lemma all_iffLR to get a one sided implication, as in *)
(* orderPcycle. *)
(*****************************************************************************)
Lemma orbitPcycle {x} : [<->
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index cd1a1bb..9953c0d 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -43,7 +43,7 @@ From mathcomp Require Import choice fintype finfun bigop.
(* is_transversal X P D <=> X is a transversal of the partition P of D. *)
(* transversal P D == a transversal of P, provided P is a partition of D. *)
(* transversal_repr x0 X B == a representative of B \in P selected by the *)
-(* tranversal X of P, or else x0. *)
+(* transversal X of P, or else x0. *)
(* powerset A == the set of all subset of the set A. *)
(* P ::&: A == those sets in P that are subsets of the set A. *)
(* f @^-1: A == the preimage of the collective predicate A under f. *)
@@ -56,7 +56,7 @@ From mathcomp Require Import choice fintype finfun bigop.
(* [set E | x in A, y in B] == the set of values of E for x drawn from A and *)
(* and y drawn from B; B may depend on x. *)
(* [set E | x <- A, y <- B & P] == the set of values of E for x drawn from A *)
-(* y drawn from B, such that P is trye. *)
+(* y drawn from B, such that P is true. *)
(* [set E | x : T] == the set of all values of E, with x in type T. *)
(* [set E | x : T & P] == the set of values of E for x : T s.t. P is true. *)
(* [set E | x : T, y : U in B], [set E | x : T, y : U in B & P], *)
@@ -102,7 +102,7 @@ From mathcomp Require Import choice fintype finfun bigop.
(* These suffixes are sometimes preceded with an `s' to distinguish them from *)
(* their basic ssrbool interpretation, e.g., *)
(* card1 : #|pred1 x| = 1 and cards1 : #|[set x]| = 1 *)
-(* We also use a trailling `r' to distinguish a right-hand complement from *)
+(* We also use a trailing `r' to distinguish a right-hand complement from *)
(* commutativity, e.g., *)
(* setIC : A :&: B = B :&: A and setICr : A :&: ~: A = set0. *)
(******************************************************************************)
@@ -146,7 +146,7 @@ Notation "{ 'set' T }" := (set_of (Phant T))
(* preferable to state equalities at the {set _} level, even when comparing *)
(* subtype values, because the primitive "injection" tactic tends to diverge *)
(* on complex types (e.g., quotient groups). We provide some parse-only *)
-(* notation to make this technicality less obstrusive. *)
+(* notation to make this technicality less obstructive. *)
Notation "A :=: B" := (A = B :> {set _})
(at level 70, no associativity, only parsing) : set_scope.
Notation "A :<>: B" := (A <> B :> {set _})
@@ -2128,7 +2128,7 @@ Qed.
(**********************************************************************)
(* *)
-(* Maximum and minimun (sub)set with respect to a given pred *)
+(* Maximum and minimum (sub)set with respect to a given pred *)
(* *)
(**********************************************************************)
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 14d623f..14faf57 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -108,7 +108,7 @@ From mathcomp Require Import path.
(* invF inj_f y == the x such that f x = y, for inj_j : injective f with *)
(* f : T -> T. *)
(* dinjectiveb A f <=> the restriction of f : T -> R to A is injective *)
-(* (this is a bolean predicate, R must be an eqType). *)
+(* (this is a boolean predicate, R must be an eqType). *)
(* injectiveb f <=> f : T -> R is injective (boolean predicate). *)
(* pred0b A <=> no x : T satisfies x \in A. *)
(* [forall x, P] <=> P (in which x can appear) is true for all values of x *)
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index f572a51..4eeada9 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -10,7 +10,7 @@ From mathcomp Require Import seq fintype.
(* provide a helper to quotient T by a decidable equivalence relation (e *)
(* : rel T) if T is a choiceType (or encodable as a choiceType modulo e). *)
(* *)
-(* See "Pragamatic Quotient Types in Coq", proceedings of ITP2013, *)
+(* See "Pragmatic Quotient Types in Coq", proceedings of ITP2013, *)
(* by Cyril Cohen. *)
(* *)
(* *** Generic Quotienting *** *)
@@ -263,7 +263,7 @@ Hypothesis pi_r : {mono \pi : x y / r x y >-> rq x y}.
Hypothesis pi_h : forall (x : T), \pi_qU (h x) = hq (\pi_qT x).
Variables (a b : T) (x : equal_to (\pi_qT a)) (y : equal_to (\pi_qT b)).
-(* Internal Lemmmas : do not use directly *)
+(* Internal Lemmas : do not use directly *)
Lemma pi_morph1 : \pi (f a) = fq (equal_val x). Proof. by rewrite !piE. Qed.
Lemma pi_morph2 : \pi (g a b) = gq (equal_val x) (equal_val y). Proof. by rewrite !piE. Qed.
Lemma pi_mono1 : p a = pq (equal_val x). Proof. by rewrite !piE. Qed.
@@ -294,7 +294,7 @@ Notation PiMono2 pi_r :=
Notation PiMorph11 pi_f :=
(fun a (x : {pi a}) => EqualTo (pi_morph11 pi_f a x)).
-(* lifiting helpers *)
+(* lifting helpers *)
Notation lift_op1 Q f := (locked (fun x : Q => \pi_Q (f (repr x)) : Q)).
Notation lift_op2 Q g :=
(locked (fun x y : Q => \pi_Q (g (repr x) (repr y)) : Q)).
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 5c8f251..259484a 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -46,7 +46,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
(* they operate on and then the operands. Here is the exhaustive list of all *)
(* such symbols for partial orders and lattices together with their default *)
(* display (as displayed by Check). We document their meaning in the *)
-(* paragraph adter the next. *)
+(* paragraph after the next. *)
(* *)
(* For porderType T *)
(* @Order.le disp T == <=%O (in fun_scope) *)
@@ -118,7 +118,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
(* `Notation "x <<< y" := @Order.lt my_display _ x y (at level ...).` *)
(* Non overloaded notations will default to the default display. *)
(* *)
-(* One may use displays either for convenience or to desambiguate between *)
+(* One may use displays either for convenience or to disambiguate between *)
(* different structures defined on "copies" of a type (as explained below.) *)
(* We provide the following "copies" of types, *)
(* the first one is a *documented example* *)
@@ -182,7 +182,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
(* the structures that fits the display one mentioned, but will rather *)
(* determine which canonical structure and display to use depending on the *)
(* copy of the type one provided. In this sense they are merely displays *)
-(* to inform the user of what the inferrence did, rather than additional *)
+(* to inform the user of what the inference did, rather than additional *)
(* input for the inference. *)
(* *)
(* Existing displays are either dual_display d (where d is a display), *)
@@ -4546,7 +4546,7 @@ Import SubOrder.Exports.
(* i.e. without creating a "copy". We use the predefined total_display, which *)
(* is designed to parse and print meet and join as minn and maxn. This looks *)
(* like standard canonical structure declaration, except we use a display. *)
-(* We also use a single factory LeOrderMixin to instanciate three different *)
+(* We also use a single factory LeOrderMixin to instantiate three different *)
(* canonical declarations porderType, distrLatticeType, orderType *)
(* We finish by providing theorems to convert the operations of ordered and *)
(* lattice types to their definition without structure abstraction. *)
@@ -4692,8 +4692,8 @@ End DvdSyntax.
(* we declare it on a "copy" of the type. *)
(* We first recover structures that are common to both nat and natdiv *)
(* (eqType, choiceType, countType) through the clone mechanisms, then we use *)
-(* a single factory MeetJoinMixin to instanciate both porderType and *)
-(* distrLatticeType canonical structures,and end with top and bottom. *)
+(* a single factory MeetJoinMixin to instantiate both porderType and *)
+(* distrLatticeType canonical structures, and end with top and bottom. *)
(* We finish by providing theorems to convert the operations of ordered and *)
(* lattice types to their definition without structure abstraction. *)
(******************************************************************************)
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. *)
(******************************************************************************)
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index d8f5939..33ea698 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -47,7 +47,7 @@ Unset Printing Implicit Defensive.
(* The complexity of any arithmetic operation with the Peano representation *)
(* is pretty dreadful, so using algorithms for "harder" problems such as *)
-(* factoring, that are geared for efficient artihmetic leads to dismal *)
+(* factoring, that are geared for efficient arithmetic leads to dismal *)
(* performance -- it takes a significant time, for instance, to compute the *)
(* divisors of just a two-digit number. On the other hand, for Peano *)
(* integers, prime factoring (and testing) is linear-time with a small *)
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index bccb968..67bc923 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -90,7 +90,7 @@ Require Export Ring.
(* V (infix) -- disjunction, as in *)
(* leq_eqVlt : (m <= n) = (m == n) || (m < n). *)
(* X - exponentiation, as in lognX : logn p (m ^ n) = logn p m * n in *)
-(* file prime.v (the suffix is not used in ths file). *)
+(* file prime.v (the suffix is not used in the file). *)
(* Suffixes that abbreviate operations (D, B, M and X) are used to abbreviate *)
(* second-rank operations in equational lemma names that describe left-hand *)
(* sides (e.g., mulnDl); they are not used to abbreviate the main operation *)
@@ -1531,7 +1531,7 @@ Section NatToNat.
Variable (f : nat -> nat).
(****************************************************************************)
-(* This listing of "Let"s factor out the required premices for the *)
+(* This listing of "Let"s factor out the required premises for the *)
(* subsequent lemmas, putting them in the context so that "done" solves the *)
(* goals quickly *)
(****************************************************************************)
@@ -1634,7 +1634,7 @@ Module NatTrec.
(* Usage: *)
(* Import NatTrec. *)
-(* in section definining functions, rebinds all *)
+(* in section defining functions, rebinds all *)
(* non-tail recursive operators. *)
(* rewrite !trecE. *)
(* in the correctness proof, restores operators *)
@@ -1782,7 +1782,7 @@ End NumberInterpretation.
(* Num 1 072 399 *)
(* to create large numbers for test cases *)
(* Eval compute in [Num of some expression] *)
-(* to display the resut of an expression that *)
+(* to display the result of an expression that *)
(* returns a larger integer. *)
Record number : Type := Num {bin_of_number :> N}.
diff --git a/mathcomp/ssreflect/ssrnotations.v b/mathcomp/ssreflect/ssrnotations.v
index dbc7f3d..d85fdf8 100644
--- a/mathcomp/ssreflect/ssrnotations.v
+++ b/mathcomp/ssreflect/ssrnotations.v
@@ -52,7 +52,7 @@ Reserved Notation "x ^- n" (at level 29, left associativity).
Reserved Notation "x *: A" (at level 40).
Reserved Notation "A :* x" (at level 40).
-(* Reserved notation for set-theretic operations. *)
+(* Reserved notation for set-theoretic operations. *)
Reserved Notation "A :&: B" (at level 48, left associativity).
Reserved Notation "A :|: B" (at level 52, left associativity).
Reserved Notation "a |: A" (at level 52, left associativity).
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index 10d54f0..ed55b08 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -373,7 +373,7 @@ Variables (n : nat) (T : finType).
(* tuple_finMixin could, in principle, be made Canonical to allow for folding *)
(* Finite.enum of a finite tuple type (see comments around eqE in eqtype.v), *)
(* but in practice it will not work because the mixin_enum projector *)
-(* has been burried under an opaque alias, to avoid some performance issues *)
+(* has been buried under an opaque alias, to avoid some performance issues *)
(* during type inference. *)
Definition tuple_finMixin := Eval hnf in FinMixin (@FinTuple.enumP n T).
Canonical tuple_finType := Eval hnf in FinType (n.-tuple T) tuple_finMixin.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:44:14 +0000