Correct spelling errors

3 files changed, 323 insertions, 0 deletions

diff --git a/debian/coq.lintian-overrides b/debian/coq.lintian-overrides
new file mode 100644
index 00000000..1c84a5d0
--- /dev/null
+++ b/debian/coq.lintian-overrides
@@ -0,0 +1,2 @@
+# False positive spelling error.
+coq binary: spelling-error-in-binary usr/bin/coqwc tage stage
diff --git a/debian/patches/0007-spelling.patch b/debian/patches/0007-spelling.patch
new file mode 100644
index 00000000..149d11b4
--- /dev/null
+++ b/debian/patches/0007-spelling.patch
@@ -0,0 +1,320 @@
+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; }
diff --git a/debian/patches/series b/debian/patches/series
index 8e94de36..b098f303 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -4,3 +4,4 @@
 0004-5127-fails-on-mips.patch
 0005-remove-ssrmatching.patch
 0006-remove-tests-that-need-coqlib.patch
+0007-spelling.patch