diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-22 11:47:16 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-22 11:47:16 -0700 |
| commit | accc9fa1f5689d1bf57d3024c4ad293fd10f3617 (patch) | |
| tree | 2a5b8e4ffa0ce872ed1fec10c91fcfdf0dfe2239 /coqprime-8.5/README.md | |
| parent | 67fc064ef8606a0efa110c5346261564fc861f11 (diff) | |
Make Coq 8.5 the default target for Fiat-Crypto
Instructions for 8.4 build in the README
Diffstat (limited to 'coqprime-8.5/README.md')
| -rw-r--r-- | coqprime-8.5/README.md | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/coqprime-8.5/README.md b/coqprime-8.5/README.md deleted file mode 100644 index 9c317fb00..000000000 --- a/coqprime-8.5/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.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 |