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

8 files changed, 6 insertions, 309 deletions

diff --git a/debian/gbp.conf b/debian/gbp.conf
index a4ee2a5f..92f87323 100644
--- a/debian/gbp.conf
+++ b/debian/gbp.conf
@@ -51,11 +51,7 @@ filter = [
     # Code with CeCILL-B license headers. bbaren believes CeCILL-B to be
     # nonfree; see
     # https://lists.debian.org/msgid-search/875zvih02a.jfx@benwick.benjamin.barenblat.name.
-    #
-    # These files will be patched in with properly licensed replacements once
-    # https://github.com/coq/coq/pull/9282 is merged.
-    "plugins/ssrmatching/ssrmatching.mli",
-    "plugins/ssrmatching/ssrmatching.v",
+    "plugins/ssrmatching/g_ssrmatching.mli",
 
     # This tries to build upstream's CI on Salsa, which doesn't work.
     ".travis.yml" ]
diff --git a/debian/patches/0006-remove-tests-that-need-coqlib.patch b/debian/patches/0005-remove-tests-that-need-coqlib.patch
index 48cd1b96..48cd1b96 100644
--- a/debian/patches/0006-remove-tests-that-need-coqlib.patch
+++ b/debian/patches/0005-remove-tests-that-need-coqlib.patch
diff --git a/debian/patches/0005-ssrmatching-license.patch b/debian/patches/0005-ssrmatching-license.patch
deleted file mode 100644
index f207cc8b..00000000
--- a/debian/patches/0005-ssrmatching-license.patch
+++ /dev/null
@@ -1,298 +0,0 @@
-From: Benjamin Barenblat <bbaren@debian.org>
-Subject: Replace deleted non-free ssrmatching files with free ones
-Forwarded: not-needed
-Last-Update: 2019-01-17
-
-Coq 8.8.2 shipped with two files in ssrmatching that were licensed under
-CeCILL-B, which I believe is a nonfree license. I've removed them from
-the Debian source package (see gbp.conf). This patch replaces them with
-equivalent files (from a later version) that are licensed freely.
-
-These files are present starting at upstream commit
-f613d9f9f0c8aec814272f6c2dcdce7e70da47b6. I've modified them by where required
-to get them to compile against 8.8.2.
---- /dev/null
-+++ b/plugins/ssrmatching/ssrmatching.mli
-@@ -0,0 +1,242 @@
-+(************************************************************************)
-+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-+(* <O___,, *       (see CREDITS file for the list of authors)           *)
-+(*   \VV/  **************************************************************)
-+(*    //   *    This file is distributed under the terms of the         *)
-+(*         *     GNU Lesser General Public License Version 2.1          *)
-+(*         *     (see LICENSE file for the text of the license)         *)
-+(************************************************************************)
-+
-+(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
-+
-+open Goal
-+open Environ
-+open Evd
-+open Constr
-+open Genintern
-+
-+(** ******** Small Scale Reflection pattern matching facilities ************* *)
-+
-+(** Pattern parsing *)
-+
-+(** The type of context patterns, the patterns of the [set] tactic and 
-+    [:] tactical. These are patterns that identify a precise subterm. *)
-+type cpattern
-+val pr_cpattern : cpattern -> Pp.t
-+
-+(** The type of rewrite patterns, the patterns of the [rewrite] tactic.
-+    These patterns also include patterns that identify all the subterms
-+    of a context (i.e. "in" prefix) *)
-+type rpattern
-+val pr_rpattern : rpattern -> Pp.t
-+
-+(** Pattern interpretation and matching *)
-+
-+exception NoMatch
-+exception NoProgress
-+
-+(** AST for [rpattern] (and consequently [cpattern]) *)
-+type ('ident, 'term) ssrpattern =
-+  | T of 'term
-+  | In_T of 'term
-+  | X_In_T of 'ident * 'term
-+  | In_X_In_T of 'ident * 'term
-+  | E_In_X_In_T of 'term * 'ident * 'term
-+  | E_As_X_In_T of 'term * 'ident * 'term
-+
-+type pattern = evar_map * (constr, constr) ssrpattern
-+val pp_pattern : pattern -> Pp.t
-+
-+(** Extracts the redex and applies to it the substitution part of the pattern.
-+  @raise Anomaly if called on [In_T] or [In_X_In_T] *)
-+val redex_of_pattern :
-+  ?resolve_typeclasses:bool -> env -> pattern ->
-+     constr Evd.in_evar_universe_context
-+
-+(** [interp_rpattern ise gl rpat] "internalizes" and "interprets" [rpat]
-+    in the current [Ltac] interpretation signature [ise] and tactic input [gl]*)
-+val interp_rpattern :
-+  goal sigma ->
-+  rpattern ->
-+    pattern
-+
-+(** [interp_cpattern ise gl cpat ty] "internalizes" and "interprets" [cpat]
-+    in the current [Ltac] interpretation signature [ise] and tactic input [gl].
-+    [ty] is an optional type for the redex of [cpat] *)
-+val interp_cpattern :
-+  goal sigma ->
-+  cpattern -> (Tacexpr.glob_constr_and_expr * Geninterp.interp_sign) option ->
-+    pattern
-+
-+(** The set of occurrences to be matched. The boolean is set to true
-+ *  to signal the complement of this set (i.e. \{-1 3\}) *)
-+type occ = (bool * int list) option
-+
-+(** [subst e p t i]. [i] is the number of binders
-+    traversed so far, [p] the term from the pattern, [t] the matched one *)
-+type subst = env -> constr -> constr -> int -> constr
-+
-+(** [eval_pattern b env sigma t pat occ subst] maps [t] calling [subst] on every
-+    [occ] occurrence of [pat]. The [int] argument is the number of 
-+    binders traversed. If [pat] is [None] then then subst is called on [t].
-+    [t] must live in [env] and [sigma], [pat] must have been interpreted in 
-+    (an extension of) [sigma]. 
-+  @raise NoMatch if [pat] has no occurrence and [b] is [true] (default [false])
-+  @return [t] where all [occ] occurrences of [pat] have been mapped using
-+    [subst] *)
-+val eval_pattern :
-+  ?raise_NoMatch:bool ->
-+  env -> evar_map -> constr ->
-+  pattern option -> occ -> subst ->
-+    constr
-+
-+(** [fill_occ_pattern b env sigma t pat occ h] is a simplified version of 
-+    [eval_pattern]. 
-+    It replaces all [occ] occurrences of [pat] in [t] with Rel [h]. 
-+    [t] must live in [env] and [sigma], [pat] must have been interpreted in 
-+    (an extension of) [sigma]. 
-+  @raise NoMatch if [pat] has no occurrence and [b] is [true] (default [false]) 
-+  @return the instance of the redex of [pat] that was matched and [t]
-+    transformed as described above. *)
-+val fill_occ_pattern :
-+  ?raise_NoMatch:bool ->
-+  env -> evar_map -> constr ->
-+  pattern -> occ -> int ->
-+    constr Evd.in_evar_universe_context * constr
-+
-+(** *************************** Low level APIs ****************************** *)
-+
-+(* The primitive matching facility. It matches of a term with holes, like 
-+   the T pattern above, and calls a continuation on its occurrences. *)
-+
-+type ssrdir = L2R | R2L
-+val pr_dir_side : ssrdir -> Pp.t
-+
-+(** a pattern for a term with wildcards *)
-+type tpattern
-+
-+(** [mk_tpattern env sigma0 sigma_p ok p_origin dir t] compiles a term [t] 
-+    living in [env] [sigma] (an extension of [sigma0]) intro a [tpattern].
-+    The [tpattern] can hold a (proof) term [p] and a diction [dir]. The [ok]
-+    callback is used to filter occurrences.
-+  @return the compiled [tpattern] and its [evar_map]
-+  @raise UserEerror is the pattern is a wildcard *)
-+val mk_tpattern :
-+  ?p_origin:ssrdir * constr ->
-+  env -> evar_map ->
-+  evar_map * constr ->
-+  (constr -> evar_map -> bool) ->
-+  ssrdir -> constr ->
-+    evar_map * tpattern
-+
-+(** [findP env t i k] is a stateful function that finds the next occurrence 
-+    of a tpattern and calls the callback [k] to map the subterm matched. 
-+    The [int] argument passed to [k] is the number of binders traversed so far 
-+    plus the initial value [i]. 
-+  @return [t] where the subterms identified by the selected occurrences of 
-+    the patter have been mapped using [k]
-+  @raise NoMatch if the raise_NoMatch flag given to [mk_tpattern_matcher] is
-+    [true] and if the pattern did not match 
-+  @raise UserEerror if the raise_NoMatch flag given to [mk_tpattern_matcher] is
-+    [false] and if the pattern did not match *)
-+type find_P =
-+  env -> constr -> int -> k:subst -> constr
-+
-+(** [conclude ()] asserts that all mentioned ocurrences have been visited.
-+  @return the instance of the pattern, the evarmap after the pattern
-+    instantiation, the proof term and the ssrdit stored in the tpattern
-+  @raise UserEerror if too many occurrences were specified *)
-+type conclude =
-+  unit -> constr * ssrdir * (evar_map * UState.t * constr)
-+
-+(** [mk_tpattern_matcher b o sigma0 occ sigma_tplist] creates a pair 
-+    a function [find_P] and [conclude] with the behaviour explained above.
-+    The flag [b] (default [false]) changes the error reporting behaviour
-+    of [find_P] if none of the [tpattern] matches. The argument [o] can
-+    be passed to tune the [UserError] eventually raised (useful if the 
-+    pattern is coming from the LHS/RHS of an equation) *)
-+val mk_tpattern_matcher :
-+  ?all_instances:bool ->
-+  ?raise_NoMatch:bool ->
-+  ?upats_origin:ssrdir * constr ->
-+  evar_map -> occ -> evar_map * tpattern list ->
-+    find_P * conclude
-+
-+(** Example of [mk_tpattern_matcher] to implement 
-+    [rewrite \{occ\}\[in t\]rules].
-+    It first matches "in t" (called [pat]), then in all matched subterms 
-+    it matches the LHS of the rules using [find_R].
-+    [concl0] is the initial goal, [concl] will be the goal where some terms
-+    are replaced by a De Bruijn index. The [rw_progress] extra check
-+    selects only occurrences that are not rewritten to themselves (e.g.
-+    an occurrence "x + x" rewritten with the commutativity law of addition 
-+    is skipped) {[
-+  let find_R, conclude = match pat with
-+  | Some (_, In_T _) ->
-+      let aux (sigma, pats) (d, r, lhs, rhs) =
-+        let sigma, pat = 
-+          mk_tpattern env0 sigma0 (sigma, r) (rw_progress rhs) d lhs in
-+        sigma, pats @ [pat] in
-+      let rpats = List.fold_left aux (r_sigma, []) rules in
-+      let find_R, end_R = mk_tpattern_matcher sigma0 occ rpats in
-+      find_R ~k:(fun _ _ h -> mkRel h), 
-+      fun cl -> let rdx, d, r = end_R () in (d,r),rdx
-+  | _ -> ... in
-+  let concl = eval_pattern env0 sigma0 concl0 pat occ find_R in
-+  let (d, r), rdx = conclude concl in ]} *)
-+
-+(* convenience shortcut: [pf_fill_occ_term gl occ (sigma,t)] returns
-+ * the conclusion of [gl] where [occ] occurrences of [t] have been replaced
-+ * by [Rel 1] and the instance of [t] *)
-+val pf_fill_occ_term : goal sigma -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t
-+
-+(* It may be handy to inject a simple term into the first form of cpattern *)
-+val cpattern_of_term : char * Tacexpr.glob_constr_and_expr -> Geninterp.interp_sign -> cpattern
-+
-+(** Helpers to make stateful closures. Example: a [find_P] function may be 
-+    called many times, but the pattern instantiation phase is performed only the
-+    first time. The corresponding [conclude] has to return the instantiated
-+    pattern redex. Since it is up to [find_P] to raise [NoMatch] if the pattern
-+    has no instance, [conclude] considers it an anomaly if the pattern did
-+    not match *)
-+
-+(** [do_once r f] calls [f] and updates the ref only once *)
-+val do_once : 'a option ref -> (unit -> 'a) -> unit
-+
-+(** [assert_done r] return the content of r. @raise Anomaly is r is [None] *)
-+val assert_done : 'a option ref -> 'a
-+
-+(** Very low level APIs.
-+    these are calls to evarconv's [the_conv_x] followed by
-+    [solve_unif_constraints_with_heuristics].
-+    In case of failure they raise [NoMatch] *)
-+
-+val unify_HO : env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map
-+val pf_unify_HO : goal sigma -> EConstr.constr -> EConstr.constr -> goal sigma
-+
-+(** Some more low level functions needed to implement the full SSR language
-+    on top of the former APIs *)
-+val tag_of_cpattern : cpattern -> char
-+val loc_of_cpattern : cpattern -> Loc.t option
-+val id_of_pattern : pattern -> Names.Id.t option
-+val is_wildcard : cpattern -> bool
-+val cpattern_of_id : Names.Id.t -> cpattern
-+val pr_constr_pat : constr -> Pp.t
-+val pf_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma
-+val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma
-+
-+(* One can also "Set SsrMatchingDebug" from a .v *)
-+val debug : bool -> unit
-+
-+val ssrinstancesof : cpattern -> Tacmach.tactic
-+
-+val profile : bool -> unit
-+val wit_cpattern : cpattern Genarg.uniform_genarg_type
-+val lcpattern : cpattern Pcoq.Gram.entry
-+val wit_lcpattern : cpattern Genarg.uniform_genarg_type
-+val cpattern : cpattern Pcoq.Gram.entry
-+val wit_rpattern : rpattern Genarg.uniform_genarg_type
-+val rpattern : rpattern Pcoq.Gram.entry
-+
-+(* eof *)
---- /dev/null
-+++ b/plugins/ssrmatching/ssrmatching.v
-@@ -0,0 +1,37 @@
-+(************************************************************************)
-+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-+(* <O___,, *       (see CREDITS file for the list of authors)           *)
-+(*   \VV/  **************************************************************)
-+(*    //   *    This file is distributed under the terms of the         *)
-+(*         *     GNU Lesser General Public License Version 2.1          *)
-+(*         *     (see LICENSE file for the text of the license)         *)
-+(************************************************************************)
-+
-+(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
-+
-+Declare ML Module "ssrmatching_plugin".
-+
-+Module SsrMatchingSyntax.
-+
-+(* Reserve the notation for rewrite patterns so that the user is not allowed  *)
-+(* to declare it at a different level.                                        *)
-+Reserved Notation "( a 'in' b )"        (at level 0).
-+Reserved Notation "( a 'as' b )"        (at level 0).
-+Reserved Notation "( a 'in' b 'in' c )" (at level 0).
-+Reserved Notation "( a 'as' b 'in' c )" (at level 0).
-+
-+Delimit Scope ssrpatternscope with pattern.
-+
-+(* Notation to define shortcuts for the "X in t" part of a pattern.           *)
-+Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope.
-+
-+(* Some shortcuts for recurrent "X in t" parts.                               *)
-+Notation RHS := (X in _ = X)%pattern.
-+Notation LHS := (X in X = _)%pattern.
-+
-+End SsrMatchingSyntax.
-+
-+Export SsrMatchingSyntax.
-+
-+Tactic Notation "ssrpattern" ssrpatternarg(p) := ssrpattern p .
diff --git a/debian/patches/0007-spelling.patch b/debian/patches/0006-spelling.patch
index 149d11b4..149d11b4 100644
--- a/debian/patches/0007-spelling.patch
+++ b/debian/patches/0006-spelling.patch
diff --git a/debian/patches/0008-avoid-usr-bin-env.patch b/debian/patches/0007-avoid-usr-bin-env.patch
index 132ed7aa..132ed7aa 100644
--- a/debian/patches/0008-avoid-usr-bin-env.patch
+++ b/debian/patches/0007-avoid-usr-bin-env.patch
diff --git a/debian/patches/0009-python-scripts-libraries.patch b/debian/patches/0008-python-scripts-libraries.patch
index 66a4a9e9..66a4a9e9 100644
--- a/debian/patches/0009-python-scripts-libraries.patch
+++ b/debian/patches/0008-python-scripts-libraries.patch
diff --git a/debian/patches/0010-skip-dot-pc.patch b/debian/patches/0009-skip-dot-pc.patch
index ce85adf8..ce85adf8 100644
--- a/debian/patches/0010-skip-dot-pc.patch
+++ b/debian/patches/0009-skip-dot-pc.patch
diff --git a/debian/patches/series b/debian/patches/series
index 7253c063..d2f569c1 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -2,9 +2,8 @@
 0002-Remove-test-4429.patch
 0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch
 0004-5127-fails-on-mips.patch
-0005-ssrmatching-license.patch
-0006-remove-tests-that-need-coqlib.patch
-0007-spelling.patch
-0008-avoid-usr-bin-env.patch
-0009-python-scripts-libraries.patch
-0010-skip-dot-pc.patch
+0005-remove-tests-that-need-coqlib.patch
+0006-spelling.patch
+0007-avoid-usr-bin-env.patch
+0008-python-scripts-libraries.patch
+0009-skip-dot-pc.patch