From accc9fa1f5689d1bf57d3024c4ad293fd10f3617 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 22 Jun 2016 11:47:16 -0700 Subject: Make Coq 8.5 the default target for Fiat-Crypto Instructions for 8.4 build in the README --- coqprime-8.4/README.md | 9 +++++++++ 1 file changed, 9 insertions(+) create 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 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 -- cgit v1.2.3