Prepare to import ssrmatching in 8.9.0

Upstream has corrected most of the licensing issues with ssrmatching
in 8.9.0. That version introduced one new file with a CeCILL-B license,
but it’s an .mli file, so OCaml should be able to infer its contents.
Don’t import the offending .mli, but do import the files with corrected
license headers. Remove the patch introduced in
5d3dc22cc205021e517a81943952655c51777083 (which backported the
correctly licensed files).

1 files changed, 320 insertions, 0 deletions

diff --git a/debian/patches/0006-spelling.patch b/debian/patches/0006-spelling.patch
new file mode 100644
index 00000000..149d11b4
--- /dev/null
+++ b/debian/patches/0006-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; }