Fix typo of caracterisation -> c*h*aracterisation

6 files changed, 12 insertions, 12 deletions

diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 56844f4773..59b2f789ab 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -333,7 +333,7 @@ Proof.
 auto with set.
 Qed.
 
-(* caracterisation of [union] via [subset] *)
+(* characterisation of [union] via [subset] *)
 
 Lemma union_subset_1: subset s (union s s')=true.
 Proof.
@@ -408,7 +408,7 @@ intros; apply equal_1; apply inter_add_2.
 rewrite not_mem_iff; auto.
 Qed.
 
-(* caracterisation of [union] via [subset] *)
+(* characterisation of [union] via [subset] *)
 
 Lemma inter_subset_1: subset (inter s s') s=true.
 Proof.
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index 1ee098cb07..4f2fdcf94c 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -333,7 +333,7 @@ Proof.
 auto with set.
 Qed.
 
-(* caracterisation of [union] via [subset] *)
+(* characterisation of [union] via [subset] *)
 
 Lemma union_subset_1: subset s (union s s')=true.
 Proof.
@@ -408,7 +408,7 @@ intros; apply equal_1; apply inter_add_2.
 rewrite not_mem_iff; auto.
 Qed.
 
-(* caracterisation of [union] via [subset] *)
+(* characterisation of [union] via [subset] *)
 
 Lemma inter_subset_1: subset (inter s s') s=true.
 Proof.
diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v
index 2da4452819..4aabda77ee 100644
--- a/theories/Numbers/Integer/Abstract/ZBits.v
+++ b/theories/Numbers/Integer/Abstract/ZBits.v
@@ -80,7 +80,7 @@ Proof.
  now apply testbit_even_succ.
 Qed.
 
-(** Alternative caracterisations of [testbit] *)
+(** Alternative characterisations of [testbit] *)
 
 (** This concise equation could have been taken as specification
    for testbit in the interface, but it would have been hard to
@@ -102,10 +102,10 @@ Proof.
  left. destruct b; split; simpl; order'.
 Qed.
 
-(** This caracterisation that uses only basic operations and
+(** This characterisation that uses only basic operations and
    power was initially taken as specification for testbit.
    We describe [a] as having a low part and a high part, with
-   the corresponding bit in the middle. This caracterisation
+   the corresponding bit in the middle. This characterisation
    is moderatly complex to implement, but also moderately
    usable... *)
 
diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v
index e1391f5990..90663de3f2 100644
--- a/theories/Numbers/Natural/Abstract/NBits.v
+++ b/theories/Numbers/Natural/Abstract/NBits.v
@@ -78,7 +78,7 @@ Proof.
  apply testbit_even_succ, le_0_l.
 Qed.
 
-(** Alternative caracterisations of [testbit] *)
+(** Alternative characterisations of [testbit] *)
 
 (** This concise equation could have been taken as specification
    for testbit in the interface, but it would have been hard to
@@ -99,10 +99,10 @@ Proof.
  destruct b; order'.
 Qed.
 
-(** This caracterisation that uses only basic operations and
+(** This characterisation that uses only basic operations and
    power was initially taken as specification for testbit.
    We describe [a] as having a low part and a high part, with
-   the corresponding bit in the middle. This caracterisation
+   the corresponding bit in the middle. This characterisation
    is moderatly complex to implement, but also moderately
    usable... *)
 
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 6a3dd97656..9b8dd1db0b 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -392,7 +392,7 @@ Definition cond_positivity (x:R) : bool :=
     | right _ => false
   end.
 
-(** Sequential caracterisation of continuity *)
+(** Sequential characterisation of continuity *)
 Lemma continuity_seq :
   forall (f:R -> R) (Un:nat -> R) (l:R),
     continuity_pt f l -> Un_cv Un l -> Un_cv (fun i:nat => f (Un i)) (f l).
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 05edc6ccde..4d04667c01 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -83,7 +83,7 @@ End GenericMinMax.
 Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
  Module Import Private_Tac := !MakeOrderTac O O.
 
-(** An alternative caracterisation of [max], equivalent to
+(** An alternative characterisation of [max], equivalent to
     [max_l /\ max_r] *)
 
 Lemma max_spec n m :