From c4ce787fddb5d8eefd96cd4706aa1ee7a8ea8843 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 2 Apr 2017 11:01:14 -0400 Subject: Remove coqprime-8.4 We're using tactics in terms in some places, and so have no hope of compiling with Coq 8.4. We no longer pretend to support it. We can probably also remove some other compatibility things, if we want. --- coqprime-8.4/README.md | 9 --------- 1 file changed, 9 deletions(-) delete mode 100644 coqprime-8.4/README.md (limited to 'coqprime-8.4/README.md') diff --git a/coqprime-8.4/README.md b/coqprime-8.4/README.md deleted file mode 100644 index 8f1b93b12..000000000 --- a/coqprime-8.4/README.md +++ /dev/null @@ -1,9 +0,0 @@ -# Coqprime (LGPL subset) - -This is a mirror of the LGPL-licensed and autogenerated files from [Coqprime](http://coqprime.gforge.inria.fr/) for Coq 8.4. It was generated from [coqprime_par.zip](https://gforge.inria.fr/frs/download.php/file/35201/coqprime_par.zip). Due to the removal of files that are missing license headers in the upstream source, `make` no longer completes successfully. However, a large part of the codebase does build and contains theorems useful to us. Fixing the build system would be nice, but is not a priority for us. - -## Usage - - make PrimalityTest/Zp.vo PrimalityTest/PocklingtonCertificat.vo - cd .. - coqide -R coqprime/Tactic Coqprime -R coqprime/N Coqprime -R coqprime/Z Coqprime -R coqprime/List Coqprime -R coqprime/PrimalityTest Coqprime YOUR_FILE.v # these are the dependencies for PrimalityTest/Zp, other modules can be added in a similar fashion -- cgit v1.2.3