Fix some documentation typos.

17 files changed, 24 insertions, 24 deletions

diff --git a/CHANGES b/CHANGES
index 97106aaf15..6b620e4a48 100644
--- a/CHANGES
+++ b/CHANGES
@@ -991,7 +991,7 @@ Extraction
   instead of accessing their body, they are now considered as axioms.
   The previous behaviour can be reactivated via the option
   "Set Extraction AccessOpaque".
-- The pretty-printer for Haskell now produces layout-independant code
+- The pretty-printer for Haskell now produces layout-independent code
 - A new command "Separate Extraction cst1 cst2 ..." that mixes a
   minimal extracted environment a la "Recursive Extraction" and the
   production of several files (one per coq source) a la "Extraction Library"
@@ -1676,7 +1676,7 @@ Tactics
   Moreover, romega now has a variant "romega with *" that can be also used
   on non-Z goals (nat, N, positive) via a call to a translation tactic named
   zify (its purpose is to Z-ify your goal...). This zify may also be used
-  independantly of romega.
+  independently of romega.
 - Tactic "remember" now supports an "in" clause to remember only selected
   occurrences of a term.
 - Tactic "pose proof" supports name overwriting in case of specialization of an
diff --git a/config/coq_config.mli b/config/coq_config.mli
index f250059316..269b68e4f6 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -37,7 +37,7 @@ val cflags : string     (* arguments passed to gcc *)
 val best : string       (* byte/opt *)
 val arch : string       (* architecture *)
 val arch_is_win32 : bool
-val osdeplibs : string  (* OS dependant link options for ocamlc *)
+val osdeplibs : string  (* OS dependent link options for ocamlc *)
 val vmbyteflags : string list (* -custom/-dllib -lcoqrun *)
 
 
@@ -56,7 +56,7 @@ val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
 val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof with Coqide *)
 
 val browser : string
-(** default web browser to use, may be overriden by environment
+(** default web browser to use, may be overridden by environment
     variable COQREMOTEBROWSER *)
 
 val has_coqide : string
diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion
index 6274275c9d..a81f170c63 100644
--- a/dev/doc/notes-on-conversion
+++ b/dev/doc/notes-on-conversion
@@ -21,7 +21,7 @@ Notation OMEGA := (ack 4 4).
 
 Definition f (x:nat) := x.
 
-(* Evaluation in tactics can somehow be controled *)
+(* Evaluation in tactics can somehow be controlled *)
 Lemma l1 : OMEGA = OMEGA.
 reflexivity.  (* succeed: identity *)
 Qed.          (* succeed: identity *)
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 48b61827d1..213fb03137 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -2587,8 +2587,8 @@ It is the language of commands of Gallina i.e. definitions, lemmas, {\ldots}
 
 \Question{What is a dependent type?}
 
-A dependant type is a type which depends on some term. For instance
-``vector of size n'' is a dependant type representing all the vectors
+A dependent type is a type which depends on some term. For instance
+``vector of size n'' is a dependent type representing all the vectors
 of size $n$. Its type depends on $n$
 
 \Question{What is a proof by reflection?}
diff --git a/ide/utils/configwin_keys.ml b/ide/utils/configwin_keys.ml
index 9f44e5c6be..e9b19da621 100644
--- a/ide/utils/configwin_keys.ml
+++ b/ide/utils/configwin_keys.ml
@@ -154,7 +154,7 @@ let xk_KP_9			= 0xFFB9
 
 
 (*
- * Auxilliary Functions; note the duplicate definitions for left and right
+ * Auxiliary Functions; note the duplicate definitions for left and right
  * function keys;  Sun keyboards and a few other manufactures have such
  * function key groups on the left and/or right sides of the keyboard.
  * We've not found a keyboard with more than 35 function keys total.
diff --git a/lib/profile.ml b/lib/profile.ml
index 2350cd43ac..13c2d9c802 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -146,9 +146,9 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
    number of allocated bytes may exceed the maximum integer capacity
    (2^31 on 32-bits architectures);  therefore, allocation is measured
    by small steps, total allocations are computed by adding elementary
-   measures and carries are controled from step to step *)
+   measures and carries are controlled from step to step *)
 
-(* Unix measure of time is approximative and shoitt delays are often
+(* Unix measure of time is approximate and short delays are often
    unperceivable; therefore, total times are measured in one (big)
    step to avoid rounding errors and to get the best possible
    approximation.
@@ -358,7 +358,7 @@ let declare_profile name =
   prof_table := (name,e)::!prof_table;
   e
 
-(* Default initialisation, may be overriden *)
+(* Default initialization, may be overridden *)
 let _ = init_profile ()
 
 (******************************)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 54e6423877..a44d942992 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -40,7 +40,7 @@ module Gram : GrammarSig
         |     (together with a constr entry level, e.g. 50, and indications of)
         |     (subentries, e.g. x in constr next level and y constr same level)
         |
-        | spliting into tokens by Metasyntax.split_notation_string
+        | splitting into tokens by Metasyntax.split_notation_string
         V
       [String "x"; String "+"; String "y"] : symbol_token list
         |
@@ -128,7 +128,7 @@ val type_of_typed_entry : typed_entry -> entry_type
 val object_of_typed_entry : typed_entry -> grammar_object Gram.entry
 val weaken_entry : 'a Gram.entry -> grammar_object Gram.entry
 
-(** Temporary activate camlp4 verbosity *)
+(** Temporarily activate camlp4 verbosity *)
 
 val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 541f299d4f..b00ecfad8a 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -610,7 +610,7 @@ module Bullet = struct
     let _ = register_behavior strict
   end
 
-  (* Current bullet behavior, controled by the option *)
+  (* Current bullet behavior, controlled by the option *)
   let current_behavior = ref Strict.strict
 
   let _ =
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 13cb559b99..5acdb7eb7e 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -8,7 +8,7 @@
 
 (** * Finite map library *)
 
-(** This file proposes an implementation of the non-dependant interface
+(** This file proposes an implementation of the non-dependent interface
  [FMapInterface.S] using lists of pairs ordered (increasing) with respect to
  left projection. *)
 
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 0f11dd7a53..130cbee871 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -8,7 +8,7 @@
 
 (** * Finite map library *)
 
-(** This file proposes an implementation of the non-dependant interface
+(** This file proposes an implementation of the non-dependent interface
  [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *)
 
 Require Import FMapInterface.
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index 1f36306c34..9c3ec71ae3 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -8,7 +8,7 @@
 
 (** * Finite sets library *)
 
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
     interface [FSetInterface.S] using strictly ordered list. *)
 
 Require Export FSetInterface.
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 2ea32e97cb..9dbea88495 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -8,7 +8,7 @@
 
 (** * Finite sets library *)
 
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
     interface [FSetInterface.WS] using lists without redundancy. *)
 
 Require Import FSetInterface.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index fb0d1ad9df..05c20eb8fa 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -8,7 +8,7 @@
 
 (** * Finite sets library *)
 
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
     interface [MSetInterface.S] using strictly ordered list. *)
 
 Require Export MSetInterface OrdersFacts OrdersLists.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 372acd56ad..2ac57a932b 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -8,7 +8,7 @@
 
 (** * Finite sets library *)
 
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
     interface [MSetWeakInterface.S] using lists without redundancy. *)
 
 Require Import MSetInterface.
diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v
index 45a7527c97..bd8930872c 100644
--- a/theories/Numbers/BigNumPrelude.v
+++ b/theories/Numbers/BigNumPrelude.v
@@ -10,7 +10,7 @@
 
 (** * BigNumPrelude *)
 
-(** Auxillary functions & theorems used for arbitrary precision efficient
+(** Auxiliary functions & theorems used for arbitrary precision efficient
     numbers. *)
 
 
@@ -22,7 +22,7 @@ Require Export Zpow_facts.
 Declare ML Module "numbers_syntax_plugin".
 
 (* *** Nota Bene ***
-   All results that were general enough has been moved in ZArith.
+   All results that were general enough have been moved in ZArith.
    Only remain here specialized lemmas and compatibility elements.
    (P.L. 5/11/2007).
 *)
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 97cb746f37..55a533c55a 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -40,7 +40,7 @@ Defined.
 
 (** * Conversion between natural numbers modulo 256 and ascii characters *)
 
-(** Auxillary function that turns a positive into an ascii by
+(** Auxiliary function that turns a positive into an ascii by
    looking at the last 8 bits, ie z mod 2^8 *)
 
 Definition ascii_of_pos : positive -> ascii :=
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c76432ae3e..1328019713 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -2050,7 +2050,7 @@ let enforce_polymorphism = function
   | None -> Flags.is_universe_polymorphism ()
   | Some b -> Flags.make_polymorphic_flag b; b
 
-(** A global default timeout, controled by option "Set Default Timeout n".
+(** A global default timeout, controlled by option "Set Default Timeout n".
     Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
 
 let default_timeout = ref None