diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-06 07:37:14 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-06 07:37:14 -0500 |
commit | 69e02ba439b2abee97315892c1354953e1c2099b (patch) | |
tree | c44d9569b2c2070937186f8b566e401ad6ad76e5 /debian/patches/ssrmatching-license.patch | |
parent | 4a85cdbc0796afd2e70a7daf30967dfa2fadbafd (diff) |
Reenable ssrmatching and ssreflect
Upstream has provided a free replacement for the nonfree ssrmatching
file I removed in cf916fd97fbac51af6fa68ec2704da2a28ef9ede. Patch that
file in and resume building ssrmatching and ssreflect.
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 |