diff options
Diffstat (limited to 'debian/patches/ssrmatching-license.patch')
| -rw-r--r-- | debian/patches/ssrmatching-license.patch | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/debian/patches/ssrmatching-license.patch b/debian/patches/ssrmatching-license.patch new file mode 100644 index 00000000..ddad1272 --- /dev/null +++ b/debian/patches/ssrmatching-license.patch @@ -0,0 +1,41 @@ +From: Benjamin Barenblat <bbaren@debian.org> +Subject: Replace deleted non-free ssrmatching file with free one +Forwarded: not-needed +Last-Update: 2019-02-06 + +Coq 8.9.0 shipped with one file in ssrmatching that was licensed under CeCILL-B, +which I believe is a nonfree license. I've removed it from the Debian source +package (see gbp.conf). This patch replaces it with an equivalent file (from a +later version) that is licensed freely. + +This file is present starting at upstream commit +b7b938a6878b754089814cbfdd478d6b9380c6bb. +--- /dev/null ++++ b/plugins/ssrmatching/g_ssrmatching.mli +@@ -0,0 +1,26 @@ ++(************************************************************************) ++(* * 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 Genarg ++open Ssrmatching ++ ++(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *) ++val cpattern : cpattern Pcoq.Entry.t ++val wit_cpattern : cpattern uniform_genarg_type ++ ++(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *) ++val lcpattern : cpattern Pcoq.Entry.t ++val wit_lcpattern : cpattern uniform_genarg_type ++ ++(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *) ++val rpattern : rpattern Pcoq.Entry.t ++val wit_rpattern : rpattern uniform_genarg_type |