From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Mon, 7 Dec 2015 10:52:14 +0100
Subject: Fix some typos.

---
 theories/Numbers/Integer/Abstract/ZDivEucl.v  | 2 +-
 theories/Numbers/Integer/Abstract/ZDivFloor.v | 2 +-
 theories/Numbers/Integer/Abstract/ZDivTrunc.v | 2 +-
 theories/Numbers/NatInt/NZDiv.v               | 2 +-
 theories/Numbers/Natural/Abstract/NDiv.v      | 2 +-
 theories/Numbers/Natural/Abstract/NParity.v   | 2 +-
 6 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'theories/Numbers')

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).
 
-- 
cgit v1.2.3