Fix some typos.

40 files changed, 93 insertions, 93 deletions

diff --git a/CHANGES b/CHANGES
index cf2bb4927..07d129a46 100644
--- a/CHANGES
+++ b/CHANGES
@@ -2180,7 +2180,7 @@ Changes from V7.3.1 to V7.4
 Symbolic notations
 
 - Introduction of a notion of scope gathering notations in a consistent set;
-  a notation sets has been developped for nat, Z and R (undocumented)
+  a notation sets has been developed for nat, Z and R (undocumented)
 - New command "Notation" for declaring notations simultaneously for
   parsing and printing (see chap 10 of the reference manual)
 - Declarations with only implicit arguments now handled (e.g. the
diff --git a/INSTALL.ide b/INSTALL.ide
index 13e741e34..6e41b2d05 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -119,5 +119,5 @@ TROUBLESHOOTING
   rid of the problem is to edit by hand your coqiderc (either
   /home/<user>/.config/coq/coqiderc under Linux, or
   C:\Documents and Settings\<user>\.config\coq\coqiderc under Windows)
-  and replace any occurence of MOD4 by MOD1.
+  and replace any occurrence of MOD4 by MOD1.
 
diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt
index 9e243eead..6a69c5793 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/univpoly.txt
@@ -167,7 +167,7 @@ kernel/univ.ml was modified. The new API forces every universe to be
 declared before it is mentionned in any constraint. This forces to
 declare every universe to be >= Set or > Set. Every universe variable
 introduced during elaboration is >= Set. Every _global_ universe is now
-declared explicitely > Set, _after_ typechecking the definition. In
+declared explicitly > Set, _after_ typechecking the definition. In
 polymorphic definitions Type@{i} ranges over Set and any other universe
 j. However, at instantiation time for polymorphic references, one can
 try to instantiate a universe parameter with Prop as well, if the
diff --git a/dev/v8-syntax/memo-v8.tex b/dev/v8-syntax/memo-v8.tex
index 8d116de26..ae4b569b3 100644
--- a/dev/v8-syntax/memo-v8.tex
+++ b/dev/v8-syntax/memo-v8.tex
@@ -253,7 +253,7 @@ became \TERM{context}. Syntax is unified with subterm matching.
 \subsection{Occurrences}
 
 To avoid ambiguity between a numeric literal and the optionnal
-occurence numbers of this term, the occurence numbers are put after
+occurrence numbers of this term, the occurrence numbers are put after
 the term itself. This applies to tactic \TERM{pattern} and also
 \TERM{unfold}
 \begin{transbox}
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index fbb866e87..2eebac39a 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -228,7 +228,7 @@ kernel is intentionally small to limit the risk of conceptual or
 accidental implementation bugs.
 \item[The Objective Caml compiler] The {\Coq} kernel is written using the
 Objective Caml language but it uses only the most standard features
-(no object, no label ...), so that it is highly unprobable that an
+(no object, no label ...), so that it is highly improbable that an
 Objective Caml bug breaks the consistency of {\Coq} without breaking all
 other kinds of features of {\Coq} or of other software compiled with
 Objective Caml.
@@ -1497,7 +1497,7 @@ while {\assert} is.
 
 \Question{What can I do if \Coq can not infer some implicit argument ?}
 
-You can state explicitely what this implicit argument is. See \ref{implicit}.
+You can state explicitly what this implicit argument is. See \ref{implicit}.
 
 \Question{How can I explicit some implicit argument ?}\label{implicit}
 
@@ -1632,7 +1632,7 @@ before comparing them, you risk to use a lot of time and space.
 
 On the contrary, a function for computing the greatest of two natural numbers
 is an algorithm  which, called on two natural numbers
-$n$ and $p$, determines wether $n\leq p$ or $p < n$.
+$n$ and $p$, determines whether $n\leq p$ or $p < n$.
 Such a function is a \emph{decision  procedure} for the inequality of
  \texttt{nat}.  The possibility of writing such a procedure comes 
 directly from de decidability of the order $\leq$ on natural numbers.
@@ -1706,7 +1706,7 @@ immediate, whereas one can't wait for  the result of
 
 This is normal. Your definition is a simple recursive function which
 returns a boolean value. Coq's \texttt{le\_lt\_dec} is a \emph{certified
-function}, i.e. a complex object, able not only to tell wether $n\leq p$
+function}, i.e. a complex object, able not only to tell whether $n\leq p$
 or $p<n$, but also of building a complete proof of the correct inequality.
 What make \texttt{le\_lt\_dec} inefficient for computing \texttt{min}
 and \texttt{max} is the building of a huge proof term.
@@ -2404,8 +2404,8 @@ You can use {\tt coqdoc}.
 
 \Question{How can I generate some dependency graph from my development?}
 
-You can use the tool \verb|coqgraph| developped by Philippe Audebaud in 2002.
-This tool transforms dependancies generated by \verb|coqdep| into 'dot' files which can be visualized using the Graphviz software (http://www.graphviz.org/).
+You can use the tool \verb|coqgraph| developed by Philippe Audebaud in 2002.
+This tool transforms dependencies generated by \verb|coqdep| into 'dot' files which can be visualized using the Graphviz software (http://www.graphviz.org/).
 
 \Question{How can I cite some {\Coq} in my latex document?}
 
@@ -2539,7 +2539,7 @@ modifiers keys available through GTK. The straightest way to get
 rid of the problem is to edit by hand your coqiderc (either
 \verb|/home/<user>/.config/coq/coqiderc| under Linux, or \\
 \verb|C:\Documents and Settings\<user>\.config\coq\coqiderc| under Windows) 
-    and replace any occurence of \texttt{MOD4} by \texttt{MOD1}.
+and replace any occurrence of \texttt{MOD4} by \texttt{MOD1}.
 
 
 
@@ -2638,7 +2638,7 @@ existential variable which eventually got erased by some computation.
 You may backtrack to the faulty occurrence of {\eauto} or {\eapply}
 and give the missing argument an explicit value. Alternatively, you
 can use the commands \texttt{Show Existentials.} and
-\texttt{Existential.} to display and instantiate the remainig
+\texttt{Existential.} to display and instantiate the remaining
 existential variables.
 
 
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 018d73908..a03d5c7b2 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -182,8 +182,8 @@ bound if it is an atomic universe (i.e. not an algebraic max()).
   experimental and is likely to change in future versions.
 \end{flushleft}
 
-The syntax has been extended to allow users to explicitely bind names to
-universes and explicitely instantantiate polymorphic
+The syntax has been extended to allow users to explicitly bind names to
+universes and explicitly instantantiate polymorphic
 definitions. Currently, binding is implicit at the first occurrence of a 
 universe name. For example, i and j below are introduced by the
 annotations attached to Types. 
@@ -202,7 +202,7 @@ definition, they just allow to specify locally what relations should
 hold. In the term and in general in proof mode, universe names
 introduced in the types can be refered to in terms.
 
-Definitions can also be instantiated explicitely, giving their full instance:
+Definitions can also be instantiated explicitly, giving their full instance:
 \begin{coq_example}
 Check (pidentity@{Set}).
 Check (le@{i j}).
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex
index 5f7b6dc95..ed1d336d9 100644
--- a/doc/tools/Translator.tex
+++ b/doc/tools/Translator.tex
@@ -419,7 +419,7 @@ the hypotheses), or a comma-separated list of either hypothesis name,
 or {\tt (value of $H$)} or {\tt (type of $H$)}. Moreover, occurrences
 can be specified after every hypothesis after the {\TERM{at}}
 keyword. {\em concl} is either empty or \TERM{*}, and can be followed
-by occurences.
+by occurrences.
 
 \begin{transbox}
 \TRANS{in Goal}{in |- *}
diff --git a/ide/coq.mli b/ide/coq.mli
index a72c67b43..2dc5ad307 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -16,7 +16,7 @@ type coqtop
     Liveness management of coqtop is automatic. Whenever a coqtop dies abruptly,
     this module is responsible for relaunching the whole process. The reset
     handler set through [set_reset_handler] will be called after such an
-    abrupt failure. It is also called when explicitely requesting coqtop to
+    abrupt failure. It is also called when explicitly requesting coqtop to
     reset. *)
 
 type 'a task
@@ -29,7 +29,7 @@ type 'a task
     ([is_computing] will answer [true]), and any other task submission
     will be rejected by [try_grab].
 
-    Any exception occuring within the task will trigger a coqtop reset.
+    Any exception occurring within the task will trigger a coqtop reset.
 
     Beware, because of the GTK scheduler, you never know when a task will
     actually be executed. If you need to sequentialize imperative actions, you
@@ -43,7 +43,7 @@ val bind : 'a task -> ('a -> 'b task) -> 'b task
 (** Monadic binding of tasks *)
 
 val lift : (unit -> 'a) -> 'a task
-(** Return the impertative computation waiting to be processed. *)
+(** Return the imperative computation waiting to be processed. *)
 
 val seq : unit task -> 'a task -> 'a task
 (** Sequential composition *)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index c0e228125..f15e5fa34 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1125,10 +1125,10 @@ let build_ui () =
 	~accel:(prefs.modifier_for_navigation^"h");*)
     item "Previous" ~label:"_Previous" ~stock:`GO_BACK
       ~callback:Nav.previous_occ
-      ~tooltip:"Previous occurence"
+      ~tooltip:"Previous occurrence"
       ~accel:(prefs.modifier_for_navigation^"less");
     item "Next" ~label:"_Next" ~stock:`GO_FORWARD ~callback:Nav.next_occ
-      ~tooltip:"Next occurence"
+      ~tooltip:"Next occurrence"
       ~accel:(prefs.modifier_for_navigation^"greater");
     item "Force" ~label:"_Force" ~stock:`EXECUTE ~callback:Nav.join_document
       ~tooltip:"Fully check the document" 
diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll
index 621833dde..4ebf9a62e 100644
--- a/ide/utf8_convert.mll
+++ b/ide/utf8_convert.mll
@@ -12,7 +12,7 @@
 
 }
 
-(* Replace all occurences of \x{iiii} and \x{iiiiiiii} by UTF-8 valid chars *)
+(* Replace all occurrences of \x{iiii} and \x{iiiiiiii} by UTF-8 valid chars *)
 
 let digit = ['0'-'9''A'-'Z''a'-'z']
 let short = digit digit digit digit
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 8298d9954..ae50b2837 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -139,7 +139,7 @@ object(self)
 
   (** We don't care about atomicity. Return:
     1. `OK when there was no error, `FAIL otherwise
-    2. `NOOP if no write occured, `WRITE otherwise
+    2. `NOOP if no write occurred, `WRITE otherwise
   *)
   method private process_action = function
   | Insert ins ->
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index a3721af66..eee928989 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -28,7 +28,7 @@ val free_vars_of_binders :
   ?bound:Id.Set.t -> Id.t list -> local_binder list -> Id.Set.t * Id.t list
 
 (** Returns the generalizable free ids in left-to-right
-   order with the location of their first occurence *)
+   order with the location of their first occurrence *)
 
 val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t ->
   glob_constr -> (Id.t * Loc.t) list
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 687b740f6..98b2d6d2e 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -481,7 +481,7 @@ and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 =
   in
   Array.equal eq_branch br1 br2
 
-(* hash_mllambda gn n env t computes the hash for t ignoring occurences of gn *)
+(* hash_mllambda gn n env t computes the hash for t ignoring occurrences of gn *)
 let rec hash_mllambda gn n env t =
   match t with
   | MLlocal ln -> combinesmall 1 (LNmap.find ln env)
@@ -979,7 +979,7 @@ let compile_prim decl cond paux =
 	let args = Array.map opt_prim_aux args in
 	app_prim (Coq_primitive(op,None)) args
 (*
-    TODO: check if this inling was useful
+    TODO: check if this inlining was useful
 	begin match op with
         | Int31lt -> 
            if Sys.word_size = 64 then
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index cb08b5058..263befd21 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -277,7 +277,7 @@ and reduce_lapp substf lids body substa largs =
   | [], _::_ -> simplify_app substf body substa (Array.of_list largs)
 
 
-(* [occurence kind k lam]:
+(* [occurrence kind k lam]:
    If [kind] is [true] return [true] if the variable [k] does not appear in 
    [lam], return [false] if the variable appear one time and not
    under a lambda, a fixpoint, a cofixpoint; else raise Not_found.
@@ -285,7 +285,7 @@ and reduce_lapp substf lids body substa largs =
    else raise [Not_found]
 *)
 
-let rec occurence k kind lam =   
+let rec occurrence k kind lam =
   match lam with
   | Lrel (_,n) -> 
       if Int.equal n k then 
@@ -294,35 +294,35 @@ let rec occurence k kind lam =
   | Lvar _  | Lconst _  | Lproj _ | Luint _ | Lval _ | Lsort _ | Lind _
   | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> kind
   | Lprod(dom, codom) ->
-      occurence k (occurence k kind dom) codom
+      occurrence k (occurrence k kind dom) codom
   | Llam(ids,body) ->
-      let _ = occurence (k+Array.length ids) false body in kind
+      let _ = occurrence (k+Array.length ids) false body in kind
   | Llet(_,def,body) ->
-      occurence (k+1) (occurence k kind def) body
+      occurrence (k+1) (occurrence k kind def) body
   | Lapp(f, args) ->
-      occurence_args k (occurence k kind f) args
+      occurrence_args k (occurrence k kind f) args
   | Lprim(_,_,_,args) | Lmakeblock(_,_,_,args) ->
-      occurence_args k kind args
+      occurrence_args k kind args
   | Lcase(_,t,a,br) ->
-      let kind = occurence k (occurence k kind t) a in
+      let kind = occurrence k (occurrence k kind t) a in
       let r = ref kind in
       Array.iter (fun (_,ids,c) -> 
-	r := occurence (k+Array.length ids) kind c && !r) br;
+	r := occurrence (k+Array.length ids) kind c && !r) br;
       !r 
   | Lif (t, bt, bf) ->
-      let kind = occurence k kind t in
-      kind && occurence k kind bt && occurence k kind bf
+      let kind = occurrence k kind t in
+      kind && occurrence k kind bt && occurrence k kind bf
   | Lfix(_,(ids,ltypes,lbodies)) 
   | Lcofix(_,(ids,ltypes,lbodies)) ->
-      let kind = occurence_args k kind ltypes in
-      let _ = occurence_args (k+Array.length ids) false lbodies in
+      let kind = occurrence_args k kind ltypes in
+      let _ = occurrence_args (k+Array.length ids) false lbodies in
       kind 
 
-and occurence_args k kind args = 
-  Array.fold_left (occurence k) kind args
+and occurrence_args k kind args =
+  Array.fold_left (occurrence k) kind args
     
 let occur_once lam = 
-  try let _ = occurence 1 true lam in true
+  try let _ = occurrence 1 true lam in true
   with Not_found -> false
       
 (* [remove_let lam] remove let expression in [lam] if the variable is *)
diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
index cefb4af89..87ef78777 100644
--- a/lib/xml_parser.mli
+++ b/lib/xml_parser.mli
@@ -36,10 +36,10 @@ type t
 
 (** Several exceptions can be raised when parsing an Xml document : {ul
         {li {!Xml.Error} is raised when an xml parsing error occurs. the
-                {!Xml.error_msg} tells you which error occured during parsing
+                {!Xml.error_msg} tells you which error occurred during parsing
                 and the {!Xml.error_pos} can be used to retreive the document
-                location where the error occured at.}
-        {li {!Xml.File_not_found} is raised when and error occured while
+                location where the error occurred at.}
+        {li {!Xml.File_not_found} is raised when and error occurred while
                 opening a file with the {!Xml.parse_file} function.}
         }
  *)
@@ -71,13 +71,13 @@ val error : error -> string
 (** Get the Xml error message as a string. *)
 val error_msg : error_msg -> string
 
-(** Get the line the error occured at. *)
+(** Get the line the error occurred at. *)
 val line : error_pos -> int
 
-(** Get the relative character range (in current line) the error occured at.*)
+(** Get the relative character range (in current line) the error occurred at.*)
 val range : error_pos -> int * int
 
-(** Get the absolute character range the error occured at. *)
+(** Get the absolute character range the error occurred at. *)
 val abs_range : error_pos -> int * int
 
 val pos : Lexing.lexbuf -> error_pos
diff --git a/library/impargs.ml b/library/impargs.ml
index 94f53219e..d15a02fea 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -104,7 +104,7 @@ let set_maximality imps b =
   inferable following a rigid path (useful to know how to print a
   partial application)
 
-- [Manual] means the argument has been explicitely set as implicit.
+- [Manual] means the argument has been explicitly set as implicit.
 
   We also consider arguments inferable from the conclusion but it is
   operational only if [conclusion_matters] is true.
diff --git a/library/impargs.mli b/library/impargs.mli
index 1d3a73e94..30f2e30f9 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -59,8 +59,8 @@ type implicit_explanation =
 	  inferable following a rigid path (useful to know how to print a
 	  partial application) *)
   | Manual
-      (** means the argument has been explicitely set as implicit. *)
-      
+      (** means the argument has been explicitly set as implicit. *)
+
 (**  We also consider arguments inferable from the conclusion but it is
      operational only if [conclusion_matters] is true. *)
 
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 8e8392961..c6d5f3b92 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -70,7 +70,7 @@ let ttree_remove ttree str =
   remove ttree 0
 
 
-(* Errors occuring while lexing (explained as "Lexer error: ...") *)
+(* Errors occurring while lexing (explained as "Lexer error: ...") *)
 
 module Error = struct
 
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index bc5a39002..ee7341a4a 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -283,7 +283,7 @@ end.
 
 (** Quotienting a polynomial by the relation X_i^2 ~ X_i *)
 
-(* Remove the multiple occurences of monomials x_k *)
+(* Remove the multiple occurrences of monomials x_k *)
 
 Fixpoint reduce_aux k p :=
 match p with
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 714cd8634..1a9080647 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -212,7 +212,7 @@ let close_previous_case pts =
     Proof.is_done pts
   then
     match get_top_stack pts with
-	Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...")
+	Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occurred ...")
       | Suppose_case :: Per (et,_,_,_) :: _ ->
 	  goto_current_focus ()
       | _ -> error "Not inside a proof per cases or induction."
diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES
index fbcd01a15..cf97ae3ab 100644
--- a/plugins/extraction/CHANGES
+++ b/plugins/extraction/CHANGES
@@ -193,7 +193,7 @@ beginning of files. Possible clashes are dealt with.
 in extracted code. 
 
 
-* A few constants are explicitely declared to be inlined in extracted code. 
+* A few constants are explicitly declared to be inlined in extracted code.
 For the moment there are: 
 	Wf.Acc_rec
 	Wf.Acc_rect
@@ -234,12 +234,12 @@ Those two commands enable a precise control of what is inlined and what is not.
 
 Print Extraction Inline. 
 
-Sum up the current state of the table recording the custom inlings 
+Sum up the current state of the table recording the custom inlinings
 (Extraction (No)Inline). 
 
 Reset Extraction Inline. 
 
-Put the table recording the custom inlings back to empty. 
+Put the table recording the custom inlinings back to empty.
 
 As a consequence, there is no more need for options inside the commands of 
 extraction: 
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 9fdb0205f..6fc1195fb 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -490,8 +490,8 @@ let ast_occurs_itvl k k' t =
     ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false
   with Found -> true
 
-(* Number of occurences of [Rel 1] in [t], with special treatment of match:
-   occurences in different branches aren't added, but we rather use max. *)
+(* Number of occurrences of [Rel 1] in [t], with special treatment of match:
+   occurrences in different branches aren't added, but we rather use max. *)
 
 let nb_occur_match =
   let rec nb k = function
@@ -851,7 +851,7 @@ let factor_branches o typ br =
     else Some (br_factor, br_set)
   end
 
-(*s If all branches are functions, try to permut the case and the functions. *)
+(*s If all branches are functions, try to permute the case and the functions. *)
 
 let rec merge_ids ids ids' = match ids,ids' with
   | [],l -> l
@@ -1127,7 +1127,7 @@ let term_expunge s (ids,c) =
       MLlam (Dummy, ast_lift 1 c)
     else named_lams ids c
 
-(*s [kill_dummy_args ids r t] looks for occurences of [MLrel r] in [t] and
+(*s [kill_dummy_args ids r t] looks for occurrences of [MLrel r] in [t] and
   purge the args of [MLrel r] corresponding to a [dummy_name].
   It makes eta-expansion if needed. *)
 
@@ -1351,10 +1351,10 @@ let is_not_strict t =
    We expand small terms with at least one non-strict
    variable (i.e. a variable that may not be evaluated).
 
-   Futhermore we don't expand fixpoints.
+   Furthermore we don't expand fixpoints.
 
-   Moreover, as mentionned by X. Leroy (bug #2241),
-   inling a constant from inside an opaque module might
+   Moreover, as mentioned by X. Leroy (bug #2241),
+   inlining a constant from inside an opaque module might
    break types. To avoid that, we require below that
    both [r] and its body are globally visible. This isn't
    fully satisfactory, since [r] might not be visible (functor),
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index bc7e6f8b0..e7732a503 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -379,7 +379,7 @@ let find_fapp (test:constr -> bool) g : fapp_info list =
 
 
 (** [finduction id filter g] tries to apply functional induction on
-    an occurence of function [id] in the conclusion of goal [g]. If
+    an occurrence of function [id] in the conclusion of goal [g]. If
     [id]=[None] then calls to any function are selected. In any case
     [heuristic] is used to select the most pertinent occurrence. *)
 let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list)
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 0f10636f0..179e8fe8d 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -6,7 +6,7 @@ open Misctypes
 val get_pattern_id : cases_pattern -> Id.t list
 
 (* [pattern_to_term pat] returns a glob_constr corresponding to [pat].
-   [pat] must not contain occurences of anonymous pattern
+   [pat] must not contain occurrences of anonymous pattern
 *)
 val pattern_to_term : cases_pattern -> glob_constr
 
@@ -64,7 +64,7 @@ val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr
 
 (* [alpha_pat avoid pat] rename all the variables present in [pat] s.t.
    the result does not share variables with [avoid]. This function create
-   a fresh variable for each occurence of the anonymous pattern.
+   a fresh variable for each occurrence of the anonymous pattern.
 
    Also returns a mapping  from old variables to new ones and the concatenation of
    [avoid] with the variables appearing in the result.
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 69e055c23..60c58730a 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -902,7 +902,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
 
 (** [merge id1 id2 args1 args2 id] builds and declares a new inductive
     type called [id], representing the merged graphs of both graphs
-    [ind1] and [ind2]. identifiers occuring in both arrays [args1] and
+    [ind1] and [ind2]. identifiers occurring in both arrays [args1] and
     [args2] are considered linked (i.e. are the same variable) in the
     new graph.
 
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index 88c1a7836..a36369d22 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -23,7 +23,7 @@ struct
 	  - None , Some v -> \]-oo,v\]
 	  - Some v, None  -> \[v,+oo\[
 	  - Some v, Some v' -> \[v,v'\]
-      Intervals needs to be explicitely normalised.
+      Intervals needs to be explicitly normalised.
       *)
 
   type who = Left | Right
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 710a2394d..aac9a7d31 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -539,7 +539,7 @@ let context operation path (t : constr) =
   in
   loop 1 path t
 
-let occurence path (t : constr) =
+let occurrence path (t : constr) =
   let rec loop p0 t = match (p0,kind_of_term t) with
     | (p, Cast (c,_,_)) -> loop p c
     | ([], _) -> t
@@ -555,7 +555,7 @@ let occurence path (t : constr) =
     | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term
     | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term
     | (p, _) ->
-	failwith ("occurence " ^ string_of_int(List.length p))
+	failwith ("occurrence " ^ string_of_int(List.length p))
   in
   loop path t
 
@@ -660,7 +660,7 @@ let clever_rewrite_gen_nat p result (t,args) =
 let clever_rewrite p vpath t gl =
   let full = pf_concl gl in
   let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in
-  let vargs = List.map (fun p -> occurence p occ) vpath in
+  let vargs = List.map (fun p -> occurrence p occ) vpath in
   let t' = applist(t, (vargs @ [abstracted])) in
   exact (applist(t',[mkNewMeta()])) gl
 
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 8156e8411..95407c5ff 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -44,7 +44,7 @@ let occ_step_eq s1 s2 = match s1, s2 with
 
 (* chemin identifiant une proposition sous forme du nom de l'hypothèse et
    d'une liste de pas à partir de la racine de l'hypothèse *)
-type occurence = {o_hyp : Names.Id.t; o_path : occ_path}
+type occurrence = {o_hyp : Names.Id.t; o_path : occ_path}
 
 (* \subsection{refiable formulas} *)
 type oformula =
@@ -81,7 +81,7 @@ and oequation = {
     e_left: oformula;			(* formule brute gauche *)
     e_right: oformula;			(* formule brute droite *)
     e_trace: Term.constr;		(* tactique de normalisation *)
-    e_origin: occurence;		(* l'hypothèse dont vient le terme *)
+    e_origin: occurrence;		(* l'hypothèse dont vient le terme *)
     e_negated: bool;			(* vrai si apparait en position nié
 					   après normalisation *)
     e_depends: direction  list;		(* liste des points de disjonction dont
@@ -111,7 +111,7 @@ type environment = {
   real_indices : (int,int) Hashtbl.t;
   mutable cnt_connectors : int;
   equations : (int,oequation) Hashtbl.t;
-  constructors : (int, occurence) Hashtbl.t
+  constructors : (int, occurrence) Hashtbl.t
 }
 
 (* \subsection{Solution tree}
@@ -136,7 +136,7 @@ type solution_tree =
    chemins pour extraire des equations ou d'hypothèses *)
 
 type context_content =
-    CCHyp of occurence
+    CCHyp of occurrence
   | CCEqua of int
 
 (* \section{Specific utility functions to handle base types} *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 8ebb037c2..d3d6901b6 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -525,7 +525,7 @@ let rec check_and_clear_in_constr env evdref err ids c =
 let clear_hyps_in_evi_main env evdref hyps terms ids =
   (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
-     the contexts of the evars occuring in evi *)
+     the contexts of the evars occurring in evi *)
   let terms =
     List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in
   let nhyps =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 8a5db9059..48911a5a9 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1011,8 +1011,8 @@ let contextually byhead occs f env sigma t =
     snd (e_contextually byhead occs f' env sigma t)
 
 (* linear bindings (following pretty-printer) of the value of name in c.
- * n is the number of the next occurence of name.
- * ol is the occurence list to find. *)
+ * n is the number of the next occurrence of name.
+ * ol is the occurrence list to find. *)
 
 let match_constr_evaluable_ref sigma c evref = 
   match kind_of_term c, evref with
@@ -1061,7 +1061,7 @@ let is_projection env = function
 
 (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
- * at the occurrences of occ_list. If occ_list is empty, unfold all occurences.
+ * at the occurrences of occ_list. If occ_list is empty, unfold all occurrences.
  * Performs a betaiota reduction after unfolding. *)
 let unfoldoccs env sigma (occs,name) c =
   let unfo nowhere_except_in locs =
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 937471cf7..5a55d47fd 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -561,7 +561,7 @@ let free_rels m =
   in
   frec 1 Int.Set.empty m
 
-(* collects all metavar occurences, in left-to-right order, preserving
+(* collects all metavar occurrences, in left-to-right order, preserving
  * repetitions and all. *)
 
 let collect_metas c =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c442178c1..5ed9ac2ba 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -88,7 +88,7 @@ type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
 type orientation = bool
 
 type conditions =
-  | Naive (* Only try the first occurence of the lemma (default) *)
+  | Naive (* Only try the first occurrence of the lemma (default) *)
   | FirstSolved (* Use the first match whose side-conditions are solved *)
   | AllMatches (* Rewrite all matches whose side-conditions are solved *)
 
@@ -1577,7 +1577,7 @@ let restrict_to_eq_and_identity eq = (* compatibility *)
 
 exception FoundHyp of (Id.t * constr * bool)
 
-(* tests whether hyp [c] is [x = t] or [t = x], [x] not occuring in [t] *)
+(* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *)
 let is_eq_x gl x (id,_,c) =
   try
     let c = pf_nf_evar gl c in
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 3e13ee570..840ede7d9 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -23,7 +23,7 @@ type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
 type orientation = bool
 
 type conditions =
-  | Naive (* Only try the first occurence of the lemma (default) *)
+  | Naive (* Only try the first occurrence of the lemma (default) *)
   | FirstSolved (* Use the first match whose side-conditions are solved *)
   | AllMatches (* Rewrite all matches whose side-conditions are solved *)
 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index efd6ded44..42d22bc3c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -124,7 +124,7 @@ let rec add_prods_sign env sigma t =
         add_prods_sign (push_named (id,Some c1,t1) env) sigma b'
     | _ -> (env,t)
 
-(* [dep_option] indicates wether the inversion lemma is dependent or not.
+(* [dep_option] indicates whether the inversion lemma is dependent or not.
    If it is dependent and I is of the form (x_bar:T_bar)(I t_bar) then
    the stated goal will be (x_bar:T_bar)(H:(I t_bar))(P t_bar H)
    where P:(x_bar:T_bar)(H:(I x_bar))[sort].
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 6bd65d0a2..081170869 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1386,7 +1386,7 @@ module Strategies =
 
 end
 
-(** The strategy for a single rewrite, dealing with occurences. *)
+(** The strategy for a single rewrite, dealing with occurrences. *)
 
 (** A dummy initial clauseenv to avoid generating initial evars before
     even finding a first application of the rewriting lemma, in setoid_rewrite
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index db3b19af5..aaa7b3a51 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -1,6 +1,6 @@
 (* Wish #2154 by E. van der Weegen *)
 
-(* auto was not using f_equal-style lemmas with metavariables occuring
+(* auto was not using f_equal-style lemmas with metavariables occurring
    only in the type of an evar of the concl, but not directly in the
    concl itself *)
 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index e0e5d94d8..0ace6938b 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -622,9 +622,9 @@ Section Elts.
   Qed.
 
 
-  (****************************************)
-  (** ** Counting occurences of a element *)
-  (****************************************)
+  (******************************************)
+  (** ** Counting occurrences of an element *)
+  (******************************************)
 
   Fixpoint count_occ (l : list A) (x : A) : nat :=
     match l with
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 4e28b5b90..f5e936cf0 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -19,7 +19,7 @@ Require Export DoubleType.
   arithmetic. In fact it is more general than that. The only reason
   for this use of 31 is the underlying mecanism for hardware-efficient
   computations by A. Spiwack. Apart from this, a switch to, say,
-  63-bit integers is now just a matter of replacing every occurences
+  63-bit integers is now just a matter of replacing every occurrences
   of 31 by 63. This is actually made possible by the use of
   dependently-typed n-ary constructions for the inductive type
   [int31], its constructor [I31] and any pattern matching on it.
diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v
index 6fdf0a2a5..376620ddc 100644
--- a/theories/Numbers/NaryFunctions.v
+++ b/theories/Numbers/NaryFunctions.v
@@ -15,7 +15,7 @@ Require Import List.
 (** * Generic dependently-typed operators about [n]-ary functions *)
 
 (** The type of [n]-ary function: [nfun A n B] is
-    [A -> ... -> A -> B] with [n] occurences of [A] in this type. *)
+    [A -> ... -> A -> B] with [n] occurrences of [A] in this type. *)
 
 Fixpoint nfun A n B :=
  match n with
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 35730eea0..48100aa7f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1359,7 +1359,7 @@ let _ =
   declare_int_option
     { optsync  = true;
       optdepr  = false;
-      optname  = "the level of inling duging functor application";
+      optname  = "the level of inlining during functor application";
       optkey   = ["Inline";"Level"];
       optread  = (fun () -> Some (Flags.get_inline_level ()));
       optwrite = (fun o ->