diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-06-10 15:01:26 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-06-10 15:03:07 -0400 |
| commit | 8d4f4adf80c7fdaa8021b283526ab1592ee13600 (patch) | |
| tree | ad05d7c38469aefd74ad9f54a5621099a1bd351f /coqprime-8.5/README.md | |
| parent | 2e566c32baf2a140cd7820c4f06437ee5c43ac44 (diff) | |
Add coqprime that works with 8.5, bundle bedrock
This simplifes the build process, and also allows us to try to build
with 8.5. We autodetect the version of Coq in the Makefile to decide
which version of coqprime to build.
Diffstat (limited to 'coqprime-8.5/README.md')
| -rw-r--r-- | coqprime-8.5/README.md | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/coqprime-8.5/README.md b/coqprime-8.5/README.md new file mode 100644 index 000000000..9c317fb00 --- /dev/null +++ b/coqprime-8.5/README.md @@ -0,0 +1,9 @@ +# Coqprime (LGPL subset) + +This is a mirror of the LGPL-licensed and autogenerated files from [Coqprime](http://coqprime.gforge.inria.fr/) for Coq 8.5. It was generated from [coqprime_8.5b.zip](https://gforge.inria.fr/frs/download.php/file/35520/coqprime_8.5b.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 |