diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-07 10:52:14 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-07 10:52:24 +0100 |
commit | df3a49a18c5b01984000df9244ecea9c275b30cd (patch) | |
tree | d14afdb5de5f93e4301f8eba8bddecd5a6597f9a /theories | |
parent | fe2776f9e0d355cccb0841495a9843351d340066 (diff) |
Fix some typos.
Diffstat (limited to 'theories')
-rw-r--r-- | theories/FSets/FMapFacts.v | 2 | ||||
-rw-r--r-- | theories/FSets/FMapPositive.v | 2 | ||||
-rw-r--r-- | theories/MMaps/MMapFacts.v | 2 | ||||
-rw-r--r-- | theories/MMaps/MMapPositive.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivFloor.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivTrunc.v | 2 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZDiv.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NDiv.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NParity.v | 2 | ||||
-rw-r--r-- | theories/Program/Subset.v | 2 | ||||
-rw-r--r-- | theories/Structures/EqualitiesFacts.v | 2 | ||||
-rw-r--r-- | theories/Structures/OrderedType.v | 2 | ||||
-rw-r--r-- | theories/Structures/OrdersLists.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zdiv.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zpow_alt.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zquot.v | 2 |
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. |