Merge branch 'v8.5'

17 files changed, 17 insertions, 17 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 8c6f4b64a..eaeb2914b 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -2143,7 +2143,7 @@ Module OrdProperties (M:S).
   Section Fold_properties.
 
   (** The following lemma has already been proved on Weak Maps,
-      but with one additionnal hypothesis (some [transpose] fact). *)
+      but with one additional hypothesis (some [transpose] fact). *)
 
   Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence  eqA)
    (f:key->elt->A->A)(i:A),
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 3eac15b03..9e59f0c50 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -1061,7 +1061,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
 End PositiveMap.
 
-(** Here come some additionnal facts about this implementation.
+(** Here come some additional facts about this implementation.
   Most are facts that cannot be derivable from the general interface. *)
 
 
diff --git a/theories/MMaps/MMapFacts.v b/theories/MMaps/MMapFacts.v
index 69066a7b6..8b356d750 100644
--- a/theories/MMaps/MMapFacts.v
+++ b/theories/MMaps/MMapFacts.v
@@ -2381,7 +2381,7 @@ Module OrdProperties (M:S).
   Section Fold_properties.
 
   (** The following lemma has already been proved on Weak Maps,
-      but with one additionnal hypothesis (some [transpose] fact). *)
+      but with one additional hypothesis (some [transpose] fact). *)
 
   Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence  eqA)
    (f:key->elt->A->A)(i:A),
diff --git a/theories/MMaps/MMapPositive.v b/theories/MMaps/MMapPositive.v
index d3aab2389..adbec7057 100644
--- a/theories/MMaps/MMapPositive.v
+++ b/theories/MMaps/MMapPositive.v
@@ -641,7 +641,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
 End PositiveMap.
 
-(** Here come some additionnal facts about this implementation.
+(** Here come some additional facts about this implementation.
   Most are facts that cannot be derivable from the general interface. *)
 
 Module PositiveMapAdditionalFacts.
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index d0df8fb4a..ab73ebfe1 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -391,7 +391,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2.
 apply add_cancel_l.
 Qed.
 
-(** Some additionnal inequalities about div. *)
+(** Some additional inequalities about div. *)
 
 Theorem div_lt_upper_bound:
   forall a b q, 0<b -> a < b*q -> a/b < q.
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index d5f3f4ada..c8260e516 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -436,7 +436,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2.
 apply add_cancel_l.
 Qed.
 
-(** Some additionnal inequalities about div. *)
+(** Some additional inequalities about div. *)
 
 Theorem div_lt_upper_bound:
   forall a b q, 0<b -> a < b*q -> a/b < q.
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index de2e99ec3..464fe354b 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -404,7 +404,7 @@ Proof.
 intros. rewrite rem_eq by order. rewrite sub_move_r; nzsimpl; tauto.
 Qed.
 
-(** Some additionnal inequalities about quot. *)
+(** Some additional inequalities about quot. *)
 
 Theorem quot_lt_upper_bound:
   forall a b q, 0<=a -> 0<b -> a < b*q -> a÷b < q.
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 4a127216f..e0dfdedbd 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -307,7 +307,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2.
 apply add_cancel_l.
 Qed.
 
-(** Some additionnal inequalities about div. *)
+(** Some additional inequalities about div. *)
 
 Theorem div_lt_upper_bound:
   forall a b q, 0<=a -> 0<b -> a < b*q -> a/b < q.
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v
index fb68c139b..d3d3eb0fb 100644
--- a/theories/Numbers/Natural/Abstract/NDiv.v
+++ b/theories/Numbers/Natural/Abstract/NDiv.v
@@ -137,7 +137,7 @@ Proof. intros; apply mul_succ_div_gt; auto'. Qed.
 Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0).
 Proof. intros. apply div_exact; auto'. Qed.
 
-(** Some additionnal inequalities about div. *)
+(** Some additional inequalities about div. *)
 
 Theorem div_lt_upper_bound:
   forall a b q, b~=0 -> a < b*q -> a/b < q.
diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v
index b3526c9a1..80a579f19 100644
--- a/theories/Numbers/Natural/Abstract/NParity.v
+++ b/theories/Numbers/Natural/Abstract/NParity.v
@@ -8,7 +8,7 @@
 
 Require Import Bool NSub NZParity.
 
-(** Some additionnal properties of [even], [odd]. *)
+(** Some additional properties of [even], [odd]. *)
 
 Module Type NParityProp (Import N : NAxiomsSig')(Import NP : NSubProp N).
 
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 50b89b5c0..ce1f7768d 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -82,7 +82,7 @@ Qed.
 Definition match_eq (A B : Type) (x : A) (fn : {y : A | y = x} -> B) : B :=
   fn (exist _ x eq_refl).
 
-(* This is what we want to be able to do: replace the originaly matched object by a new,
+(* This is what we want to be able to do: replace the originally matched object by a new,
    propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *)
 
 Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B)
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index 8e2b2d081..d5827d87a 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -60,7 +60,7 @@ Module KeyDecidableType(D:DecidableType).
 
  Hint Resolve eqke_1 eqke_2 eqk_1.
 
- (* Additionnal facts *)
+ (* Additional facts *)
 
  Lemma InA_eqke_eqk {elt} p (m:list (key*elt)) :
    InA eqke p m -> InA eqk p m.
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index cc8c2261b..93ca383b2 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -342,7 +342,7 @@ Module KeyOrderedType(O:OrderedType).
    compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto.
   Qed.
 
-  (* Additionnal facts *)
+  (* Additional facts *)
 
   Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'.
    Proof.
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
index 4d49ac84e..41e65d728 100644
--- a/theories/Structures/OrdersLists.v
+++ b/theories/Structures/OrdersLists.v
@@ -76,7 +76,7 @@ Module KeyOrderedType(O:OrderedType).
  Instance ltk_compat' {elt} : Proper (eqke==>eqke==>iff) (@ltk elt).
  Proof. eapply subrelation_proper; eauto with *. Qed.
 
- (* Additionnal facts *)
+ (* Additional facts *)
 
  Instance pair_compat {elt} : Proper (O.eq==>Logic.eq==>eqke) (@pair key elt).
  Proof. apply pair_compat. Qed.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index d0d10891a..363b4fd03 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -279,7 +279,7 @@ Proof. intros; rewrite Z.div_exact; auto. Qed.
 Theorem Zmod_le: forall a b, 0 < b -> 0 <= a -> a mod b <= a.
 Proof. intros. apply Z.mod_le; auto. Qed.
 
-(** Some additionnal inequalities about Z.div. *)
+(** Some additional inequalities about Z.div. *)
 
 Theorem Zdiv_lt_upper_bound:
   forall a b q, 0 < b -> a < q*b -> a/b < q.
diff --git a/theories/ZArith/Zpow_alt.v b/theories/ZArith/Zpow_alt.v
index 8f661a9c8..c8627477b 100644
--- a/theories/ZArith/Zpow_alt.v
+++ b/theories/ZArith/Zpow_alt.v
@@ -11,7 +11,7 @@ Local Open Scope Z_scope.
 
 (** An alternative power function for Z *)
 
-(** This [Zpower_alt] is extensionnaly equal to [Z.pow],
+(** This [Zpower_alt] is extensionally equal to [Z.pow],
     but not convertible with it. The number of
     multiplications is logarithmic instead of linear, but
     these multiplications are bigger. Experimentally, it seems
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index 3ef111898..6db92edb7 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -243,7 +243,7 @@ Proof. intros. zero_or_not b. intuition. apply Z.quot_exact; auto. Qed.
 Theorem Zrem_le a b : 0 <= a -> 0 <= b -> Z.rem a b <= a.
 Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed.
 
-(** Some additionnal inequalities about Zdiv. *)
+(** Some additional inequalities about Zdiv. *)
 
 Theorem Zquot_le_upper_bound:
   forall a b q, 0 < b -> a <= q*b -> a÷b <= q.