Correct some spelling errors

Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)

This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.

19 files changed, 41 insertions, 41 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 794804a1f6..26f4ec6242 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -103,7 +103,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms:
 
   .. exn:: Not the right number of missing arguments.
 
-.. _occurencessets:
+.. _occurrencessets:
 
 Occurrence sets and occurrence clauses
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1024,7 +1024,7 @@ Managing the local context
       This notation allows specifying which occurrences of :token:`term` have
       to be substituted in the context. The :n:`in @goal_occurrences` clause
       is an occurrence clause whose syntax and behavior are described in
-      :ref:`goal occurences <occurencessets>`.
+      :ref:`goal occurrences <occurrencessets>`.
 
    .. tacv:: set (@ident @binders := @term) {? in @goal_occurrences }
 
@@ -1509,7 +1509,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       This syntax is used for selecting which occurrences of :token:`term`
       the case analysis has to be done on. The :n:`in @goal_occurrences`
       clause is an occurrence clause whose syntax and behavior is described
-      in :ref:`occurences sets <occurencessets>`.
+      in :ref:`occurrences sets <occurrencessets>`.
 
    .. tacv:: destruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences }
              edestruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences }
@@ -1659,7 +1659,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    This syntax is used for selecting which occurrences of :n:`@term` the
    induction has to be carried on. The :n:`in @goal_occurrences` clause is an
    occurrence clause whose syntax and behavior is described in
-   :ref:`occurences sets <occurencessets>`. If variables or hypotheses not
+   :ref:`occurrences sets <occurrencessets>`. If variables or hypotheses not
    mentioning :n:`@term` in their type are listed in :n:`@goal_occurrences`,
    those are generalized as well in the statement to prove.
 
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex
index 3ee65d6f22..d8ac640f2a 100644
--- a/doc/tools/Translator.tex
+++ b/doc/tools/Translator.tex
@@ -490,7 +490,7 @@ to be applied are separated by a {\tt =>}.
 to turn implicit only the arguments that are {\em strictly} implicit
 (or rigid), i.e. that remains inferable whatever the other arguments
 are. For instance {\tt x} inferable from {\tt P x} is not strictly
-inferable since it can disappears if {\tt P} is instanciated by a term
+inferable since it can disappears if {\tt P} is instantiated by a term
 which erases {\tt x}.
 
 \begin{transbox}
diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml
index 2be5dce426..002722ace9 100644
--- a/ide/nanoPG.ml
+++ b/ide/nanoPG.ml
@@ -189,7 +189,7 @@ let emacs = insert emacs "Emacs" [] [
       run "Edit" "Cut";
       { s with kill = Some(txt,false); sel = false }
     else s));
-  mkE _k "k" "Kill untill the end of line" (Edit(fun s b i _ ->
+  mkE _k "k" "Kill until the end of line" (Edit(fun s b i _ ->
     let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in
     let k =
       if i#ends_line then begin
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index c21ce22421..1e4dbfd418 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -764,7 +764,7 @@ and lambda_of_app env f args =
                               and such, which can't be done at this time.
                               for instance, for int31: if one of the digit is
                                   not closed, it's not impossible that the number
-                                  gets fully instanciated at run-time, thus to ensure
+                                  gets fully instantiated at run-time, thus to ensure
                                   uniqueness of the representation in the vm
                                   it is necessary to try and build a caml integer
                                   during the execution *)
diff --git a/lib/future.ml b/lib/future.ml
index 7a5b6f699b..b372bedc5d 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -49,7 +49,7 @@ end
 module UUIDMap = Map.Make(UUID)
 module UUIDSet = Set.Make(UUID)
 
-type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
+type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
 
 (* Val is not necessarily a final state, so the
    computation restarts from the state stocked into Val *)
@@ -103,7 +103,7 @@ let from_here ?(fix_exn=id) v = create fix_exn (Val v)
 let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn
 
 let create_delegate ?(blocking=true) ~name fix_exn =
-  let assignement signal ck = fun v ->
+  let assignment signal ck = fun v ->
     let _, _, fix_exn, c = get ck in
     assert (match !c with Delegated _ -> true | _ -> false);
     begin match v with
@@ -118,7 +118,7 @@ let create_delegate ?(blocking=true) ~name fix_exn =
     (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock),
     (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in
   let ck = create ~name fix_exn (Delegated wait) in
-  ck, assignement signal ck
+  ck, assignment signal ck
 
 (* TODO: get rid of try/catch to be stackless *)
 let rec compute ck : 'a value =
diff --git a/lib/future.mli b/lib/future.mli
index d9e8c87b21..55f05518b0 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -70,10 +70,10 @@ val fix_exn_of : 'a computation -> fix_exn
 (* Run remotely, returns the function to assign.
    If not blocking (the default) it raises NotReady if forced before the
    delegate assigns it. *)
-type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
+type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
 val create_delegate :
   ?blocking:bool -> name:string ->
-  fix_exn -> 'a computation * ('a assignement -> unit)
+  fix_exn -> 'a computation * ('a assignment -> unit)
 
 (* Given a computation that is_exn, replace it by another one *)
 val replace : 'a computation -> 'a computation -> unit
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index b12364d04a..98d68d3db7 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -638,11 +638,11 @@ let my_orelse tac1 tac2 g =
 (*     observe (str "using snd tac since : " ++ CErrors.print e); *)
     tac2 g
 
-let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
+let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
   let args = Array.of_list (List.map mkVar  args_id) in
-  let instanciate_one_hyp hid =
+  let instantiate_one_hyp hid =
     my_orelse
-      ( (* we instanciate the hyp if possible  *)
+      ( (* we instantiate the hyp if possible  *)
 	fun g ->
 	  let prov_hid = pf_get_new_id hid g in
 	  let c = mkApp(mkVar hid,args) in
@@ -678,7 +678,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
     tclTHENLIST
       [
 	tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps;
-	tclMAP instanciate_one_hyp hyps;
+        tclMAP instantiate_one_hyp hyps;
 	(fun g ->
 	   let all_g_hyps_id =
 	     List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty
@@ -722,11 +722,11 @@ let build_proof
 			 tclTHENLIST [Proofview.V82.of_tactic (Simple.case t);
 				     (fun g' ->
 					let g'_nb_prod = nb_prod (project g') (pf_concl g') in
-					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
+                                        let nb_instantiate_partial = g'_nb_prod - g_nb_prod in
 			 		observe_tac "treat_new_case"
 					  (treat_new_case
 					     ptes_infos
-					     nb_instanciate_partial
+                                             nb_instantiate_partial
 					     (build_proof do_finalize)
 					     t
 					     dyn_infos)
@@ -760,7 +760,7 @@ let build_proof
 				  nb_rec_hyps  = List.length new_hyps
 			       }
 			   in
-(* 			   observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
+(* 			   observe_tac "Lambda" *) (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
 			     (* 			   build_proof do_finalize new_infos g' *)
 			) g
 		  | _ ->
@@ -1120,7 +1120,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	in
 	(full_params, (* real params *)
 	 princ_params, (* the params of the principle which are not params of the function *)
-	 substl (* function instanciated with real params *)
+         substl (* function instantiated with real params *)
 	   (List.map var_of_decl full_params)
 	   f_body
 	)
@@ -1130,7 +1130,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	let f_body = compose_lam f_ctxt_other f_body in
 	(princ_info.params, (* real params *)
 	 [],(* all params are full params *)
-	 substl (* function instanciated with real params *)
+         substl (* function instantiated with real params *)
 	   (List.map var_of_decl princ_info.params)
 	   f_body
 	)
@@ -1321,7 +1321,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 (* 			   str "args := " ++ prlist_with_sep spc Ppconstr.pr_id  args_id *)
 
 (* 			   ); *)
-		     (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac
+                     (* observe_tac "instancing" *) (instantiate_hyps_with_args prove_tac
 		       (List.rev_map id_of_decl princ_info.branches)
 		       (List.rev args_id))
 		   ]
@@ -1371,7 +1371,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 			 do_prove
 			 dyn_infos
 		    in
-		    instanciate_hyps_with_args prove_tac
+                    instantiate_hyps_with_args prove_tac
 		       (List.rev_map id_of_decl princ_info.branches)
 		      (List.rev args_id)
 		   ]
@@ -1728,8 +1728,8 @@ let prove_principle_for_gen
 	     ptes_info
 	     (body_info rec_hyps)
 	 in
-	 (* observe_tac "instanciate_hyps_with_args"  *)
-	   (instanciate_hyps_with_args
+         (* observe_tac "instantiate_hyps_with_args"  *)
+           (instantiate_hyps_with_args
 	      make_proof
 	      (List.map (get_name %> Nameops.Name.get_id) princ_info.branches)
 	      (List.rev args_ids)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 89dfb58017..9fa333c629 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1320,7 +1320,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
     | None   ->
 	try add_suffix current_proof_name "_subproof"
 	with e when CErrors.noncritical e ->
-          anomaly (Pp.str "open_new_goal with an unamed theorem.")
+          anomaly (Pp.str "open_new_goal with an unnamed theorem.")
   in
   let na = next_global_ident_away name Id.Set.empty in
   if Termops.occur_existential sigma gls_type then
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 094adfda7a..94a3d40441 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -183,7 +183,7 @@ Ltac zify_nat_op :=
         let t := eval compute in (Z.of_nat (S a)) in
         change (Z.of_nat (S a)) with t in H
       | _ => rewrite (Nat2Z.inj_succ a) in H
-      | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]),
+      | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]),
                 hide [Z.of_nat (S a)] in this one hypothesis *)
         change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H
      end
@@ -194,7 +194,7 @@ Ltac zify_nat_op :=
         let t := eval compute in (Z.of_nat (S a)) in
         change (Z.of_nat (S a)) with t
       | _ => rewrite (Nat2Z.inj_succ a)
-      | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]),
+      | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]),
                 hide [Z.of_nat (S a)] in the goal *)
         change (Z.of_nat (S a)) with (Z_of_nat' (S a))
      end
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 2510c16934..7bca7c7099 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -178,7 +178,7 @@ let rec display_action print_var = function
       | DIVIDE_AND_APPROX (e1,e2,k,d) ->
           Printf.printf
             "Inequation E%d is divided by %s and the constant coefficient is \
-            rounded by substracting %s.\n" e1.id (sbi k) (sbi d)
+            rounded by subtracting %s.\n" e1.id (sbi k) (sbi d)
       | NOT_EXACT_DIVIDE (e,k) ->
           Printf.printf
             "Constant in equation E%d is not divisible by the pgcd \
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index aadb4fe5f6..4a63dd4708 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -856,7 +856,7 @@ let rec uniquize = function
   let p' = mkApp (pf, pa) in
   if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t)
   else errorstrm (str"Only " ++ int !nocc ++ str" < " ++ int max_occ ++
-        str(String.plural !nocc " occurence") ++ match upats_origin with
+        str(String.plural !nocc " occurrence") ++ match upats_origin with
         | None -> str" of" ++ spc() ++ pr_constr_pat p'
         | Some (dir,rule) -> str" of the " ++ pr_dir_side dir ++ fnl() ++
             ws 4 ++ pr_constr_pat p' ++ fnl () ++ 
diff --git a/stm/stm.ml b/stm/stm.ml
index b7ba163309..19915b1600 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1364,7 +1364,7 @@ module rec ProofTask : sig
     t_stop     : Stateid.t;
     t_drop     : bool;
     t_states   : competence;
-    t_assign   : Proof_global.closed_proof_output Future.assignement -> unit;
+    t_assign   : Proof_global.closed_proof_output Future.assignment -> unit;
     t_loc      : Loc.t option;
     t_uuid     : Future.UUID.t;
     t_name     : string }
@@ -1403,7 +1403,7 @@ end = struct (* {{{ *)
     t_stop     : Stateid.t;
     t_drop     : bool;
     t_states   : competence;
-    t_assign   : Proof_global.closed_proof_output Future.assignement -> unit;
+    t_assign   : Proof_global.closed_proof_output Future.assignment -> unit;
     t_loc      : Loc.t option;
     t_uuid     : Future.UUID.t;
     t_name     : string }
@@ -1843,7 +1843,7 @@ and TacTask : sig
   type task = {
     t_state    : Stateid.t;
     t_state_fb : Stateid.t;
-    t_assign   : output Future.assignement -> unit;
+    t_assign   : output Future.assignment -> unit;
     t_ast      : int * aast;
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
@@ -1860,7 +1860,7 @@ end = struct (* {{{ *)
   type task = {
     t_state    : Stateid.t;
     t_state_fb : Stateid.t;
-    t_assign   : output Future.assignement -> unit;
+    t_assign   : output Future.assignment -> unit;
     t_ast      : int * aast;
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
diff --git a/test-suite/bugs/closed/bug_4132.v b/test-suite/bugs/closed/bug_4132.v
index 806ffb771f..67ecc3087f 100644
--- a/test-suite/bugs/closed/bug_4132.v
+++ b/test-suite/bugs/closed/bug_4132.v
@@ -26,6 +26,6 @@ Qed.
 
 Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b.
 omega. (* Pierre L: according to a comment of bug report #4132,
-          this might have triggered "Failure(occurence 2)" in the past,
+          this might have triggered "Failure(occurrence 2)" in the past,
           but I never managed to reproduce that. *)
 Qed.
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index 2863404590..28426b5700 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -60,7 +60,7 @@ Qed.
 
 Record U : Type := { A:=Type; a:A }.
 
-(** Check assignement of sorts to inductives and records. *)
+(** Check assignment of sorts to inductives and records. *)
 
 Variable sh : list nat.
 
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index c3bdf656d1..0e56cc3c0f 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -59,7 +59,7 @@ let usage_coq_makefile () =
 \n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\
 \n as a dependencies of an already defined target \"foo\".\
 \n[-I dir]: look for Objective Caml dependencies in \"dir\"\
-\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\
+\n[-R physicalpath logicalpath]: look for Coq dependencies recursively\
 \n  starting from \"physicalpath\". The logical path associated to the\
 \n  physical path is \"logicalpath\".\
 \n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 8ec8927abd..606d954672 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -71,7 +71,7 @@ let is_tactic =
     [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
       "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; 
       "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
-      "info"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto";
+      "info"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto";
       "quote"; "eexact"; "autorewrite";
       "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
       "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml
index 68aadcfccf..bfea141bb3 100644
--- a/tools/coqworkmgr.ml
+++ b/tools/coqworkmgr.ml
@@ -169,7 +169,7 @@ let main () =
     "-j",Arg.Set_int max_tokens, "max number of concurrent jobs";
     "-d",Arg.Set debug, "do not detach (debug)"] in
   let usage =
-    "Prints on stdout an env variable assignement to be picked up by coq\n"^
+    "Prints on stdout an env variable assignment to be picked up by coq\n"^
     "instances in order to limit the maximum number of concurrent workers.\n"^
     "The default value is 2.\n"^
     "Usage:" in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index ab898644c0..cea8af3f05 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -244,7 +244,7 @@ let do_program_recursive local poly fixkind fixl ntns =
     interp_recursive ~cofix ~program_mode:true fixl ntns
   in
     (* Program-specific code *)
-    (* Get the interesting evars, those that were not instanciated *)
+    (* Get the interesting evars, those that were not instantiated *)
   let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
     (* Solve remaining evars *)
   let evd = nf_evar_map_undefined evd in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index bdf74bf63d..5352cf5f8c 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -348,7 +348,7 @@ open Goptions
 let _ =
   declare_bool_option
     { optdepr  = false;
-      optname  = "Hidding of Program obligations";
+      optname  = "Hiding of Program obligations";
       optkey   = ["Hide";"Obligations"];
       optread  = get_hide_obligations;
       optwrite = set_hide_obligations; }