Correct some spelling errorsmaster

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`.

20 files changed, 47 insertions, 47 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 9b4d724e0..d1a685307 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -113,15 +113,15 @@ Occurrence sets and occurrence clauses
 An occurrence clause is a modifier to some tactics that obeys the
 following syntax:
 
-.. _tactic_occurence_grammar:
+.. _tactic_occurrence_grammar:
 
   .. productionlist:: `sentence`
-     occurence_clause : in `goal_occurences`
-     goal_occurences : [ident [`at_occurences`], ... , ident [`at_occurences`] [|- [* [`at_occurences`]]]]
-                      :| * |- [* [`at_occurences`]]
-                      :| *
+     occurrence_clause : in `goal_occurrences`
+     goal_occurrences : [ident [`at_occurrences`], ... , ident [`at_occurrences`] [|- [* [`at_occurrences`]]]]
+                       :| * |- [* [`at_occurrences`]]
+                       :| *
      at_occurrences : at `occurrences`
-     occurences     : [-] `num` ... `num`
+     occurrences     : [-] `num` ... `num`
 
 The role of an occurrence clause is to select a set of occurrences of a term in
 a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate that
@@ -1002,7 +1002,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
    This notation allows  specifying which occurrences of :n:`@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 <occurencessets>`.
 
 .. tacv:: set (@ident {+ @binder} := @term )
 
@@ -1483,7 +1483,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    This syntax is used for selecting which occurrences of :n:`@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>`.
+   :ref:`occurrences sets <occurencessets>`.
 
 .. tacv:: destruct @term with @bindings_list as @disj_conj_intro_pattern eqn:@naming_intro_pattern using @term with @bindings_list in @goal_occurrences
 .. tacv:: edestruct @term with @bindings_list as @disj_conj_intro_pattern eqn:@naming_intro_pattern using @term with @bindings_list in @goal_occurrences
@@ -1631,7 +1631,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 <occurencessets>`. 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 3ee65d6f2..d8ac640f2 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 2be5dce42..002722ace 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 f1b6f3dff..32a4bd650 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -763,7 +763,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 7a5b6f699..b372bedc5 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 d9e8c87b2..55f05518b 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 533694864..3154154ff 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 7298342e1..118bcde8b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1318,7 +1318,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 59fd9b801..bc31cb98e 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -181,7 +181,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
@@ -192,7 +192,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 2510c1693..7bca7c709 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/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 51b99b993..f4ac202f2 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1866,7 +1866,7 @@ Qed.
 
 End IntOmega.
 
-(** For now, the above modular construction is instanciated on Z,
+(** For now, the above modular construction is instantiated on Z,
     in order to retrieve the initial ROmega. *)
 
 Module ZOmega := IntOmega(Z_as_Int).
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 05eda14e9..13ff817df 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -853,7 +853,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 e15b6048b..6827ec03f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1334,7 +1334,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 }
@@ -1373,7 +1373,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 }
@@ -1813,7 +1813,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;
@@ -1830,7 +1830,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/4132.v b/test-suite/bugs/closed/4132.v
index 806ffb771..67ecc3087 100644
--- a/test-suite/bugs/closed/4132.v
+++ b/test-suite/bugs/closed/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 286340459..28426b570 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 ad489da82..33ced97ed 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -48,7 +48,7 @@ let usage_common () =
 \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 05bc6aea9..750698a1c 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -76,7 +76,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 68aadcfcc..bfea141bb 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 102a98f04..ad21a6d9e 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -255,7 +255,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 14d764232..abea7ff9d 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -342,7 +342,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; }