8 files changed, 14 insertions, 14 deletions
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 3c9b6b428b..dcaea894eb 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -15,7 +15,7 @@
     It follows the implementation from Ocaml's standard library,
 
     All operations given here expect and produce well-balanced trees
-    (in the ocaml sense: heigths of subtrees shouldn't differ by more
+    (in the ocaml sense: heights of subtrees shouldn't differ by more
     than 2), and hence has low complexities (e.g. add is logarithmic
     in the size of the set). But proving these balancing preservations
     is in fact not necessary for ensuring correct operational behavior
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/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 9d2a73ed0f..95868861fa 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -13,7 +13,7 @@
     This module factorizes common parts in implementations
     of finite sets as AVL trees and as Red-Black trees. The nodes
     of the trees defined here include an generic information
-    parameter, that will be the heigth in AVL trees and the color
+    parameter, that will be the height in AVL trees and the color
     in Red-Black trees. Without more details here about these
     information parameters, trees here are not known to be
     well-balanced, but simply binary-search-trees.
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 :