fix typos in documentation: text

1 files changed, 5 insertions, 5 deletions

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         *)
 (*                                                                    *)
 (**********************************************************************)