| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
|
| |
As of 8.9, upstream has stopped distributing plugins that turn coqtop
into worker processes for CoqIDE and other things. There are now
separate binaries for each coqtop use case. Ensure they’re all
distributed.
|
| |
|
|
|
|
|
|
| |
The nonfree file in ssrmatching I removed in
cf916fd97fbac51af6fa68ec2704da2a28ef9ede turns out to be important to
the build process, and I can’t figure out how to replicate its effects
without including the file itself. Disable ssrmatching and ssreflect
again until the license situation gets resolved.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
4181269ff800d58e60b886d0aaa2894444a9cd0d removed ssrmatching and
everything that needed it because upstream had shipped a couple of
files with bad license headers. Those files have now been fixed
(https://github.com/coq/coq/pull/9282), so grab them from master and
apply them in a patch. This restores ssrmatching to the Coq standard
library.
Once upstream cuts its next release, we should be able to delete the
patch and simply import the files from the upstream tarball.
|
| | |
|
| |
|
|
|
|
|
| |
ssrmatching has two files licensed under CeCILL-B, which I believe is a
nonfree license. d7d80c5bea564b7cb0eadc33e9ee38c9d9de1cd8 removed those
files from the source package; this commit disables the affected plugin
in the build system.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
Benjamin Barenblat
Enrico Tassi
Stephane Glondu