From 5d3dc22cc205021e517a81943952655c51777083 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Thu, 17 Jan 2019 19:58:25 -0500 Subject: Restore ssrmatching and its reverse dependencies 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. --- debian/libcoq-ocaml.install.in | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'debian/libcoq-ocaml.install.in') diff --git a/debian/libcoq-ocaml.install.in b/debian/libcoq-ocaml.install.in index c89a0e53..44d87c81 100644 --- a/debian/libcoq-ocaml.install.in +++ b/debian/libcoq-ocaml.install.in @@ -21,6 +21,8 @@ usr/lib/coq/plugins/syntax/nat_syntax_plugin.cmo usr/lib/coq/plugins/syntax/ascii_syntax_plugin.cmo usr/lib/coq/plugins/syntax/string_syntax_plugin.cmo usr/lib/coq/plugins/syntax/z_syntax_plugin.cmo +usr/lib/coq/plugins/ssr/ssreflect_plugin.cmo +usr/lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmo usr/lib/coq/toploop/proofworkertop.cma usr/lib/coq/toploop/tacworkertop.cma usr/lib/coq/toploop/queryworkertop.cma @@ -49,3 +51,5 @@ DYN: usr/lib/coq/plugins/syntax/r_syntax_plugin.cmxs DYN: usr/lib/coq/plugins/syntax/int31_syntax_plugin.cmxs DYN: usr/lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs DYN: usr/lib/coq/plugins/syntax/string_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/ssr/ssreflect_plugin.cmxs +DYN: usr/lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmxs -- cgit v1.2.3