Fixing typos - Part 3

32 files changed, 34 insertions, 34 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 7f26181108..8abd4a3cbb 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -76,7 +76,7 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70).
 
 (** Decidable leibniz equality instances. *)
 
-(** The equiv is burried inside the setoid, but we can recover it by specifying
+(** The equiv is buried inside the setoid, but we can recover it by specifying
    which setoid we're talking about. *)
 
 Program Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index f6b240bf20..28394b984e 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -77,7 +77,7 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70).
 
 Require Import Coq.Arith.Arith.
 
-(** The equiv is burried inside the setoid, but we can recover
+(** The equiv is buried inside the setoid, but we can recover
   it by specifying which setoid we're talking about. *)
 
 Program Instance eq_setoid A : Setoid A | 10 :=
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index 8970529103..a12e4a43c2 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -192,7 +192,7 @@ Module Type WSfun (E : DecidableType).
     (** Equality of maps *)
 
     (** Caveat: there are at least three distinct equality predicates on maps.
-      - The simpliest (and maybe most natural) way is to consider keys up to
+      - The simplest (and maybe most natural) way is to consider keys up to
         their equivalence [E.eq], but elements up to Leibniz equality, in
         the spirit of [eq_key_elt] above. This leads to predicate [Equal].
       - Unfortunately, this [Equal] predicate can't be used to describe
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 83bb07ffb6..d977ac05ec 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -240,7 +240,7 @@ the above form:
       True.
     Proof.
       intros. push not in *.
-       (* note that ~(R->P) remains (since R isnt decidable) *)
+       (* note that ~(R->P) remains (since R isn't decidable) *)
       tauto.
     Qed.
 
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 1a391ed799..d54c8bf42d 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -37,7 +37,7 @@ Notation "~ x" := (not x) : type_scope.
 Register not as core.not.type.
 
 (** Create the "core" hint database, and set its transparent state for
-  variables and constants explicitely. *)
+  variables and constants explicitly. *)
 
 Create HintDb core.
 Hint Variables Opaque : core.
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index 7e7a1ced58..5952f3a31b 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -331,7 +331,7 @@ Definition iter (n:nat) {A} (f:A->A) (x:A) : A :=
 (** Bitwise operations *)
 
 (** We provide here some bitwise operations for unary numbers.
-  Some might be really naive, they are just there for fullfiling
+  Some might be really naive, they are just there for fulfilling
   the same interface as other for natural representations. As
   soon as binary representations such as NArith are available,
   it is clearly better to convert to/from them and use their ops.
diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v
index 419a0be49c..e1e0d3db4c 100644
--- a/theories/Lists/StreamMemo.v
+++ b/theories/Lists/StreamMemo.v
@@ -70,7 +70,7 @@ Qed.
 End MemoFunction.
 
 (** For a dependent function, the previous solution is
-    reused thanks to a temporarly hiding of the dependency
+    reused thanks to a temporary hiding of the dependency
     in a "container" [memo_val]. *)
 
 Section DependentMemoFunction.
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index b06384e992..73d7432193 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -385,7 +385,7 @@ End Proof_irrelevance_EM_CC.
     fragment of [Prop] into [bool], hence weak classical logic,
     i.e. [forall A, ~A\/~~A], is enough for deriving a weak version of
     proof-irrelevance. This is enough to derive a contradiction from a
-    [Set]-bound weak excluded middle wih an impredicative [Set]
+    [Set]-bound weak excluded middle with an impredicative [Set]
     universe. *)
 
 Section Proof_irrelevance_WEM_CC.
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index f228cbb3bf..3ceff849be 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -240,7 +240,7 @@ the above form:
       True.
     Proof.
       intros. push not in *.
-       (* note that ~(R->P) remains (since R isnt decidable) *)
+       (* note that ~(R->P) remains (since R isn't decidable) *)
       tauto.
     Qed.
 
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index a3dcca7dfd..838721f499 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -166,7 +166,7 @@ end.
 *)
 
 (** Enumeration of the elements of a tree. This corresponds
-    to the "samefringe" notion in the litterature. *)
+    to the "samefringe" notion in the literature. *)
 
 #[universes(template)]
 Inductive enumeration :=
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index 6a18f59fc4..85139593da 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -659,7 +659,7 @@ End Raw2Sets.
 (** It is in fact possible to provide an ordering on sets with
     very little information on them (more or less only the [In]
     predicate). This generic build of ordering is in fact not
-    used for the moment, we rather use a simplier version
+    used for the moment, we rather use a simpler version
     dedicated to sets-as-sorted-lists, see [MakeListOrdering].
 *)
 
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index be12fffaaf..3e5987127a 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -25,7 +25,7 @@ Module N.
 
 Definition t := N.
 
-(** ** Nicer name [N.pos] for contructor [Npos] *)
+(** ** Nicer name [N.pos] for constructor [Npos] *)
 
 Notation pos := Npos.
 
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/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.
 *)
 
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 7f30733559..1c78011941 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -310,7 +310,7 @@ Infix "<?" := ltb (at level 70, no associativity) : positive_scope.
 
 (** ** A Square Root function for positive numbers *)
 
-(** We procede by blocks of two digits : if p is written qbb'
+(** We proceed by blocks of two digits : if p is written qbb'
     then sqrt(p) will be sqrt(q)~0 or sqrt(q)~1.
     For deciding easily in which case we are, we store the remainder
     (as a mask, since it can be null).
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 5ae933d433..9fe3b967ae 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -31,7 +31,7 @@ Definition block {A : Type} (a : A) := a.
 Ltac block_goal := match goal with [ |- ?T ] => change (block T) end.
 Ltac unblock_goal := unfold block in *.
 
-(** Notation for heterogenous equality. *)
+(** Notation for heterogeneous equality. *)
 
 Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
 
@@ -88,7 +88,7 @@ Ltac elim_eq_rect :=
       end
   end.
 
-(** Rewrite using uniqueness of indentity proofs [H = eq_refl]. *)
+(** Rewrite using uniqueness of identity proofs [H = eq_refl]. *)
 
 Ltac simpl_uip :=
   match goal with
@@ -450,7 +450,7 @@ Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l)
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => destruct hyp using c) H.
 
 (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by 
-   writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before
+   writing another wrapper calling do_depelim. We suppose the hyp has to be generalized before
    calling [induction]. *)
 
 Tactic Notation "dependent" "induction" ident(H) :=
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index ec283b886e..c41ab905e0 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1352,7 +1352,7 @@ Proof.
 Qed.
 
 (*********************************************************)
-(** ** Order and substraction                            *)
+(** ** Order and subtraction                            *)
 (*********************************************************)
 
 Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0.
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 08bc400f0a..142883a525 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -543,7 +543,7 @@ Qed.
 End Permut_permut.
 
 (* begin hide *)
-(** For compatibilty *)
+(** For compatibility *)
 Notation permut_right := permut_cons (only parsing).
 Notation permut_tran := permut_trans (only parsing).
 (* end hide *)
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index d000b75bf4..e5b2e22dc1 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -208,7 +208,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
   unfold eqb; intros; destruct (eq_dec x y); elim_comp; auto.
   Qed.
 
-(* Specialization of resuts about lists modulo. *)
+(* Specialization of results about lists modulo. *)
 
 Section ForNotations.
 
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 182b781fe1..354c1eb9b0 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -431,7 +431,7 @@ Proof.
 apply eq_true_iff_eq. now rewrite negb_true_iff, ltb_lt, leb_gt.
 Qed.
 
-(** Relation bewteen [compare] and the boolean comparisons *)
+(** Relation between [compare] and the boolean comparisons *)
 
 Lemma eqb_compare x y :
  (x =? y) = match compare x y with Eq => true | _ => false end.
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v
index ebd8ee8fc2..80925ff058 100644
--- a/theories/Structures/OrdersTac.v
+++ b/theories/Structures/OrdersTac.v
@@ -51,7 +51,7 @@ Local Infix "+" := trans_ord.
 
    This used to be provided here via a [TotalOrder], but
    for technical reasons related to extraction, we now ask
-   for two sperate parts: relations in a [EqLtLe] + properties in
+   for two separate parts: relations in a [EqLtLe] + properties in
    [IsTotalOrder]. Note that [TotalOrder = EqLtLe <+ IsTotalOrder]
 *)
 
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index 4088843a1b..0b3e9b78f6 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -160,7 +160,7 @@ Qed.
  
 (** The p{^ th} element of [fin m] viewed as the p{^ th} element of
 [fin (n + m)]
-Really really ineficient !!! *)
+Really really inefficient !!! *)
 Definition L_R {m} n (p : t m) : t (n + m).
 Proof.
 induction n.
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.