diff options
Diffstat (limited to 'coqprime-8.4/README.md')
| -rw-r--r-- | coqprime-8.4/README.md | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/coqprime-8.4/README.md b/coqprime-8.4/README.md new file mode 100644 index 000000000..8f1b93b12 --- /dev/null +++ b/coqprime-8.4/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.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 |