Fixing typos - Part 3

4 files changed, 4 insertions, 4 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index a346ab8ccb..43841920e5 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1259,7 +1259,7 @@ Proof.
  f_equal. now rewrite <- add_assoc, add_opp_diag_r, add_0_r.
 Qed.
 
-(** * [testbit] in terms of comparision. *)
+(** * [testbit] in terms of comparison. *)
 
 Lemma testbit_mod_pow2 a n i (H : 0 <= n)
   : testbit (a mod 2 ^ n) i = ((i <? n) && testbit a i)%bool.
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index 8cb62622db..a9a5f15f2e 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -28,7 +28,7 @@ Module Z.
 
 Definition t := Z.
 
-(** ** Nicer names [Z.pos] and [Z.neg] for contructors *)
+(** ** Nicer names [Z.pos] and [Z.neg] for constructors *)
 
 Notation pos := Zpos.
 Notation neg := Zneg.
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 0b0ed48d51..9cade75f08 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -13,7 +13,7 @@
 (** We define a signature for an integer datatype based on [Z].
     The goal is to allow a switch after extraction to ocaml's
     [big_int] or even [int] when finiteness isn't a problem
-    (typically : when mesuring the height of an AVL tree).
+    (typically : when measuring the height of an AVL tree).
 *)
 
 Require Import BinInt.
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index a619eb90ef..64431a9411 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -105,7 +105,7 @@ Proof.
     rewrite Z.rem_sign_nz; trivial. apply Z.square_nonneg.
 Qed.
 
-(** This can also be said in a simplier way: *)
+(** This can also be said in a simpler way: *)
 
 Theorem Zrem_sgn2 a b : 0 <= (Z.rem a b) * a.
 Proof.