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

6 files changed, 19 insertions, 19 deletions

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 () ++