Fix some typos.

31 files changed, 52 insertions, 52 deletions

diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 6630be06a..64431ea16 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -81,7 +81,7 @@ Parenthesis are used to group regexps. Beware to distinguish this operator
 $\GR{~}$ from the terminals $\ETERM{( )}$, and $\mid$ from terminal
 \TERMbar.
 
-Rules are optionaly annotated in the right margin with:
+Rules are optionally annotated in the right margin with:
 \begin{itemize}
 \item a precedence and associativity (L for left, R for right and N for no associativity), indicating how to solve conflicts;
   lower levels are tighter;
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 8e078e981..3a99bfdd4 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -201,7 +201,7 @@ in their context. In this case, the obligations should be transparent
 recursive calls can be checked by the
 kernel's type-checker. There is an optimization in the generation of
 obligations which gets rid of the hypothesis corresponding to the
-functionnal when it is not necessary, so that the obligation can be
+functional when it is not necessary, so that the obligation can be
 declared opaque (e.g. using {\tt Qed}). However, as soon as it appears in the
 context, the proof of the obligation is \emph{required} to be declared transparent.
 
@@ -216,7 +216,7 @@ properties. It will generate obligations, try to solve them
 automatically and fail if some unsolved obligations remain. 
 In this case, one can first define the lemma's
 statement using {\tt Program Definition} and use it as the goal afterwards.
-Otherwise the proof will be started with the elobarted version as a goal.
+Otherwise the proof will be started with the elaborated version as a goal.
 The {\tt Program} prefix can similarly be used as a prefix for {\tt Variable}, {\tt
   Hypothesis}, {\tt Axiom} etc...
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 55b5f622f..f367f04c4 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3555,7 +3555,7 @@ The hints for \texttt{auto} and \texttt{eauto} are stored in
 databases.  Each database maps head symbols to a list of hints. One can
 use the command \texttt{Print Hint \ident} to display the hints
 associated to the head symbol \ident{} (see \ref{PrintHint}). Each
-hint has a cost that is an nonnegative integer, and an optional pattern.
+hint has a cost that is a nonnegative integer, and an optional pattern.
 The hints with lower cost are tried first. A hint is tried by
 \texttt{auto} when the conclusion of the current goal
 matches its pattern or when it has no pattern.
@@ -3772,7 +3772,7 @@ Hint Extern 4 (~(_ = _)) => discriminate.
   with hints with a cost less than 4.
 
   One can even use some sub-patterns of the pattern in the tactic
-  script. A sub-pattern is a question mark followed by an ident, like
+  script. A sub-pattern is a question mark followed by an identifier, like
   \texttt{?X1} or \texttt{?X2}. Here is an example:
 
 % Require EqDecide.
@@ -3815,7 +3815,7 @@ The \texttt{emp} regexp does not match any search path while
 \texttt{eps} matches the empty path. During proof search, the path of
 successive successful hints on a search branch is recorded, as a list of
 identifiers for the hints (note \texttt{Hint Extern}'s do not have an
-associated identitier). Before applying any hint $\ident$ the current
+associated identifier). Before applying any hint $\ident$ the current
 path $p$ extended with $\ident$ is matched against the current cut
 expression $c$ associated to the hint database. If matching succeeds,
 the hint is \emph{not} applied. The semantics of \texttt{Hint Cut} $e$
@@ -4672,7 +4672,7 @@ Use \texttt{classical\_right} to prove the right part of the disjunction with th
 %% procedure for first-order intuitionistic logic implemented in {\em
 %%   NuPRL}\cite{Kre02}.
 
-%% Search may optionnaly be bounded by a multiplicity parameter
+%% Search may optionally be bounded by a multiplicity parameter
 %% indicating how many (at most) copies of a formula may be used in
 %% the proof process, its absence may lead to non-termination of the tactic.
 
diff --git a/kernel/closure.ml b/kernel/closure.ml
index ea9b2755f..03e70495f 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -771,7 +771,7 @@ let drop_parameters depth n argstk =
   (* we know that n < stack_args_size(argstk) (if well-typed term) *) 
   anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor")
 
-(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding 
+(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding
     to the conversion of the eta expansion of t, considered as an inhabitant 
     of ind, and the Constructor c of this inductive type applied to arguments
     s.
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 063c9cf12..b625478f2 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -33,7 +33,7 @@ let check_constraints cst env =
   if Environ.check_constraints cst env then ()
   else error_unsatisfied_constraints env cst
 
-(* This should be a type (a priori without intension to be an assumption) *)
+(* This should be a type (a priori without intention to be an assumption) *)
 let type_judgment env c t =
   match kind_of_term(whd_betadeltaiota env t) with
     | Sort s -> {utj_val = c; utj_type = s }
@@ -52,8 +52,8 @@ let assumption_of_judgment env t ty =
     error_assumption env (make_judge t ty)
 
 (************************************************)
-(* Incremental typing rules: builds a typing judgement given the *)
-(* judgements for the subterms. *)
+(* Incremental typing rules: builds a typing judgment given the *)
+(* judgments for the subterms. *)
 
 (*s Type of sorts *)
 
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 0609c8517..009ff82ff 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -11,9 +11,9 @@ open Term
 open Mod_subst
 
 (** This module implements the handling of opaque proof terms.
-    Opauqe proof terms are special since:
+    Opaque proof terms are special since:
     - they can be lazily computed and substituted
-    - they are stoked in an optionally loaded segment of .vo files
+    - they are stored in an optionally loaded segment of .vo files
     An [opaque] proof terms holds the real data until fully discharged.
     In this case it is called [direct].
     When it is [turn_indirect] the data is relocated to an opaque table
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 6ae519ef6..1112c3b89 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -734,7 +734,7 @@ and extract_cst_app env mle mlt kn u args =
   if la >= ls
   then
     (* Enough args, cleanup already done in [mla], we only add the
-       additionnal dummy if needed. *)
+       additional dummy if needed. *)
     put_magic_if (magic2 && not magic1) (mlapp head (optdummy @ mla))
   else
     (* Partially applied function with some logical arg missing.
@@ -748,7 +748,7 @@ and extract_cst_app env mle mlt kn u args =
 (*s Extraction of an inductive constructor applied to arguments. *)
 
 (* \begin{itemize}
-   \item In ML, contructor arguments are uncurryfied.
+   \item In ML, constructor arguments are uncurryfied.
    \item We managed to suppress logical parts inside inductive definitions,
    but they must appears outside (for partial applications for instance)
    \item We also suppressed all Coq parameters to the inductives, since
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 61fce267a..34ce66967 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -8,7 +8,7 @@ val prove_princ_for_struct :
 
 
 val prove_principle_for_gen :
-  constant*constant*constant -> (* name of the function, the fonctionnal and the fixpoint equation *)
+  constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *)
   constr option ref -> (* a pointer to the obligation proofs lemma *)
   bool -> (* is that function uses measure *)
   int -> (* the number of recursive argument *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5d41ec723..951bef2be 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -203,7 +203,7 @@ let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> glob
 
 
 
-(* Debuging mechanism *)
+(* Debugging mechanism *)
 let debug_queue = Stack.create ()
 
 let rec print_debug_queue b e = 
@@ -291,9 +291,9 @@ let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
 
   
 
-(* Travelling term.
+(* Traveling term.
    Both definitions of [f_terminate] and [f_equation] use the same generic 
-   travelling mechanism.
+   traveling mechanism.
 *)
 
 (* [check_not_nested forbidden e] checks that [e] does not contains any variable 
@@ -327,7 +327,7 @@ let check_not_nested forbidden e =
   with UserError(_,p) -> 
     errorlabstrm "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p)
 
-(* ['a info] contains the local information for travelling *)
+(* ['a info] contains the local information for traveling *)
 type 'a infos = 
     { nb_arg : int; (* function number of arguments *)
       concl_tac : tactic; (* final tactic to finish proofs *)
@@ -337,7 +337,7 @@ type 'a infos =
       f_id : Id.t;  (* function name *)
       f_constr : constr;  (* function term *)
       f_terminate : constr; (* termination proof term *)
-      func : global_reference; (* functionnal reference *)
+      func : global_reference; (* functional reference *)
       info : 'a;
       is_main_branch : bool; (* on the main branch or on a matched expression *)
       is_final : bool; (* final first order term or not *)
@@ -357,7 +357,7 @@ type ('a,'b) journey_info_tac =
     'b infos -> (* argument of the tactic *)
     tactic
        
-(* journey_info : specifies the actions to do on the different term constructors during the travelling of the term
+(* journey_info : specifies the actions to do on the different term constructors during the traveling of the term
 *)
 type journey_info = 
     { letiN : ((Name.t*constr*types*constr),constr) journey_info_tac;
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 95407c5ff..560e6a899 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -46,7 +46,7 @@ let occ_step_eq s1 s2 = match s1, s2 with
    d'une liste de pas à partir de la racine de l'hypothèse *)
 type occurrence = {o_hyp : Names.Id.t; o_path : occ_path}
 
-(* \subsection{refiable formulas} *)
+(* \subsection{reifiable formulas} *)
 type oformula =
     (* integer *)
   | Oint of Bigint.bigint
@@ -55,7 +55,7 @@ type oformula =
   | Omult of oformula * oformula
   | Ominus of oformula * oformula
   | Oopp of  oformula
-    (* an atome in the environment *)
+    (* an atom in the environment *)
   | Oatom of int
     (* weird expression that cannot be translated *)
   | Oufo of oformula
@@ -75,7 +75,7 @@ type oproposition =
   | Pimp of int * oproposition * oproposition
   | Pprop of Term.constr
 
-(* Les équations ou proposiitions atomiques utiles du calcul *)
+(* Les équations ou propositions atomiques utiles du calcul *)
 and oequation = {
     e_comp: comparaison;		(* comparaison *)
     e_left: oformula;			(* formule brute gauche *)
@@ -1266,7 +1266,7 @@ let resolution env full_reified_goal systems_list =
       |	(O_right :: l) -> app coq_p_right [| loop l |] in
     let correct_index =
       let i = List.index0 Names.Id.equal e.e_origin.o_hyp l_hyps in
-      (* PL: it seems that additionnally introduced hyps are in the way during
+      (* PL: it seems that additionally introduced hyps are in the way during
              normalization, hence this index shifting... *)
       if Int.equal i 0 then 0 else Pervasives.(+) i (List.length to_introduce)
     in
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index b92b847be..56023bfb5 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -155,7 +155,7 @@ Section ZMORPHISM.
    Ltac norm := gen_srewrite Rsth Reqe ARth.
    Ltac add_push := gen_add_push radd Rsth Reqe ARth.
 
-(*morphisms are extensionaly equal*)
+(*morphisms are extensionally equal*)
  Lemma same_genZ : forall x, [x] == gen_phiZ1 x.
  Proof.
   destruct x;simpl; try rewrite (same_gen ARth);rrefl.
@@ -246,7 +246,7 @@ Proof (SRth_ARth Nsth Nth).
 Lemma Neqb_ok : forall x y, N.eqb x y = true -> x = y.
 Proof. exact (fun x y => proj1 (N.eqb_eq x y)). Qed.
 
-(**Same as above : definition of two,extensionaly equal, generic morphisms *)
+(**Same as above : definition of two, extensionally equal, generic morphisms *)
 (**from N to any semi-ring*)
 Section NMORPHISM.
  Variable R : Type.
@@ -671,7 +671,7 @@ End GEN_DIV.
    end.
 
 (* A simple tactic recognizing only 0 and 1. The inv_gen_phiX above
-   are only optimisations that directly returns the reifid constant
+   are only optimisations that directly returns the reified constant
    instead of resorting to the constant propagation of the simplification
    algorithm. *)
 Ltac inv_gen_phi rO rI cO cI t :=
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index c40e0ffba..c2eafcdad 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -42,7 +42,7 @@ Defined.
 
 (*Instance ZEquality: @Equality Z:= (@eq Z).*)
 
-(** Two generic morphisms from Z to (abrbitrary) rings, *)
+(** Two generic morphisms from Z to (arbitrary) rings, *)
 (**second one is more convenient for proofs but they are ext. equal*)
 Section ZMORPHISM.
 Context {R:Type}`{Ring R}.
@@ -130,7 +130,7 @@ Ltac rsimpl := simpl.
  Qed.
 
 
-(*morphisms are extensionaly equal*)
+(*morphisms are extensionally equal*)
  Lemma same_genZ : forall x, [x] == gen_phiZ1 x.
  Proof.
   destruct x;rsimpl; try rewrite same_gen; reflexivity.
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3e6cea5dd..ce8b9b3db 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3205,7 +3205,7 @@ let make_abstract_generalize gl id concl dep ctx body c eqs args refls =
 	mkProd (Anonymous, eq, lift 1 concl), [| refl |]
     else concl, [||]
   in
-    (* Abstract by equalitites *)
+    (* Abstract by equalities *)
   let eqs = lift_togethern 1 eqs in (* lift together and past genarg *)
   let abseqs = it_mkProd_or_LetIn (lift eqslen abshypeq) (List.map (fun x -> (Anonymous, None, x)) eqs) in
     (* Abstract by the "generalized" hypothesis. *)
@@ -3216,11 +3216,11 @@ let make_abstract_generalize gl id concl dep ctx body c eqs args refls =
   let genc = mkCast (mkMeta meta, DEFAULTcast, genctyp) in
     (* Apply the old arguments giving the proper instantiation of the hyp *)
   let instc = mkApp (genc, Array.of_list args) in
-    (* Then apply to the original instanciated hyp. *)
+    (* Then apply to the original instantiated hyp. *)
   let instc = Option.cata (fun _ -> instc) (mkApp (instc, [| mkVar id |])) body in
     (* Apply the reflexivity proofs on the indices. *)
   let appeqs = mkApp (instc, Array.of_list refls) in
-    (* Finaly, apply the reflexivity proof for the original hyp, to get a term of type gl again. *)
+    (* Finally, apply the reflexivity proof for the original hyp, to get a term of type gl again. *)
     mkApp (appeqs, abshypt)
 
 let hyps_of_vars env sign nogen hyps =
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 7150d1fd4..207f25ed0 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -352,7 +352,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v
           fi; \
 	} > "$@"
 
-# Additionnal dependencies for module tests
+# Additional dependencies for module tests
 $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo
 modules/%.vo: modules/%.v
 	$(HIDE)$(coqtop) -R modules Mods -compile $<
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.