path: root/debian/patches/0006-spelling.patch

From: Benjamin Barenblat <bbaren@google.com>
Subject: Correct some spelling errors
Origin: backport, https://github.com/coq/coq/commit/06cd051d140a183229cd43f0bbae152d6ad8d6ca
Reviewed-by: Benjamin Barenblat <bbaren@debian.org>

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`.
--- a/ide/nanoPG.ml
+++ b/ide/nanoPG.ml
@@ -189,7 +189,7 @@
       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
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -767,7 +767,7 @@
                               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 *)
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -49,7 +49,7 @@
 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 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 @@
     (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 =
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -70,10 +70,10 @@
 (* 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
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -638,11 +638,11 @@
 (*     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 @@
     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 @@
 			 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 @@
 				  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
 		  | _ ->
@@ -1118,7 +1118,7 @@
 	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
 	)
@@ -1128,7 +1128,7 @@
 	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
 	)
@@ -1319,7 +1319,7 @@
 (* 			   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))
 		   ]
@@ -1369,7 +1369,7 @@
 			 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)
 		   ]
@@ -1726,8 +1726,8 @@
 	     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)
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1318,7 +1318,7 @@
     | 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
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -181,7 +181,7 @@
         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 @@
         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
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -178,7 +178,7 @@
       | 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 \
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1343,7 +1343,7 @@
     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 }
@@ -1381,7 +1381,7 @@
     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 }
@@ -1819,7 +1819,7 @@
   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;
@@ -1836,7 +1836,7 @@
   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;
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -60,7 +60,7 @@
 
 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.
 
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -59,7 +59,7 @@
 \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\
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -76,7 +76,7 @@
     [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
       "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; 
       "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
-      "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto";
+      "info"; "fourier"; "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";
--- a/tools/coqworkmgr.ml
+++ b/tools/coqworkmgr.ml
@@ -169,7 +169,7 @@
     "-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
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -254,7 +254,7 @@
     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
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -338,7 +338,7 @@
 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; }