9 files changed, 11 insertions, 11 deletions
diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v
index c7e3999691..6809154a33 100644
--- a/theories/Numbers/AltBinNotations.v
+++ b/theories/Numbers/AltBinNotations.v
@@ -18,7 +18,7 @@
     thousands of digits and more, conversion from/to [Decimal.int] can
     become significantly slow. If that becomes a problem for your
     development, this file provides some alternative [Numeral
-    Notation] commmands that use [Z] as bridge type. To enable these
+    Notation] commands that use [Z] as bridge type. To enable these
     commands, just be sure to [Require] this file after other files
     defining numeral notations.
 
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 4b0bda3d44..a7bc4211ed 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1288,7 +1288,7 @@ Section Int31_Specs.
  intros; rewrite <- spec_1; apply spec_add.
  Qed.
 
- (** Substraction *)
+ (** Subtraction *)
 
  Lemma spec_sub_c : forall x y, [-|sub31c x y|] = [|x|] - [|y|].
  Proof.
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index b9185c9ca0..10f819b005 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -255,7 +255,7 @@ Definition add31carryc (n m : int31) :=
   | _ => C1 npmpone
   end.
 
-(** * Substraction *)
+(** * Subtraction *)
 
 (** Subtraction modulo [2^31] *)
 
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index 4bcd22543f..94da55b3f3 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -372,7 +372,7 @@ Section ZModulo.
  assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)).
   unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
  generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l).
- destruct 1; injection H as ? ?.
+ destruct 1; injection H as [= ? ?].
  rewrite H0.
  assert ([|l|] = l).
   apply Zmod_small; auto.
@@ -414,7 +414,7 @@ Section ZModulo.
   unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
  generalize (Z_div_mod [|a|] [|b|] H0).
  destruct Z.div_eucl as (q,r); destruct 1; intros.
- injection H1 as ? ?.
+ injection H1 as [= ? ?].
  assert ([|r|]=r).
   apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
    auto with zarith.
@@ -525,7 +525,7 @@ Section ZModulo.
   unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
  generalize (Z_div_mod a [|b|] H3).
  destruct Z.div_eucl as (q,r); destruct 1; intros.
- injection H4 as ? ?.
+ injection H4 as [= ? ?].
  assert ([|r|]=r).
   apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
    auto with zarith.
diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v
index 4aabda77ee..42ea8f76fb 100644
--- a/theories/Numbers/Integer/Abstract/ZBits.v
+++ b/theories/Numbers/Integer/Abstract/ZBits.v
@@ -324,7 +324,7 @@ Proof.
  now rewrite <- opp_succ, opp_nonneg_nonpos, le_succ_l.
 Qed.
 
-(** Accesing a high enough bit of a number gives its sign *)
+(** Accessing a high enough bit of a number gives its sign *)
 
 Lemma bits_iff_nonneg : forall a n, log2 (abs a) < n ->
  (0<=a <-> a.[n] = false).
diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v
index 0ab528de80..377c05e279 100644
--- a/theories/Numbers/Integer/Abstract/ZLcm.v
+++ b/theories/Numbers/Integer/Abstract/ZLcm.v
@@ -207,7 +207,7 @@ Qed.
 
    We had an abs in order to have an always-nonnegative lcm,
    in the spirit of gcd. Nota: [lcm 0 0] should be 0, which
-   isn't garantee with the third equation above.
+   isn't guarantee with the third equation above.
 *)
 
 Definition lcm a b := abs (a*(b/gcd a b)).
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index 5f102e853b..b96a2b35af 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -149,7 +149,7 @@ Proof.
 intros n m H; apply add_le_cases; now nzsimpl.
 Qed.
 
-(** Substraction *)
+(** Subtraction *)
 
 (** We can prove the existence of a subtraction of any number by
     a smaller one *)
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index acebfcf1d2..cace65c61d 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -310,7 +310,7 @@ Qed.
 End NZOfNatOrd.
 
 
-(** For basic operations, we can prove correspondance with
+(** For basic operations, we can prove correspondence with
     their counterpart in [nat]. *)
 
 Module NZOfNatOps (Import NZ:NZAxiomsSig').
diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v
index 47b74193ed..19a8b4b2b1 100644
--- a/theories/Numbers/Natural/Abstract/NLcm.v
+++ b/theories/Numbers/Natural/Abstract/NLcm.v
@@ -90,7 +90,7 @@ Qed.
             = (a / gcd a b) * b
             = (a*b) / gcd a b
 
-   Nota: [lcm 0 0] should be 0, which isn't garantee with the third
+   Nota: [lcm 0 0] should be 0, which isn't guarantee with the third
    equation above.
 *)