aboutsummaryrefslogtreecommitdiff
path: root/coqprime/README.md
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2016-06-22 11:47:16 -0700
committerGravatar Jason Gross <jagro@google.com>2016-06-22 11:47:16 -0700
commitaccc9fa1f5689d1bf57d3024c4ad293fd10f3617 (patch)
tree2a5b8e4ffa0ce872ed1fec10c91fcfdf0dfe2239 /coqprime/README.md
parent67fc064ef8606a0efa110c5346261564fc861f11 (diff)
Make Coq 8.5 the default target for Fiat-Crypto
Instructions for 8.4 build in the README
Diffstat (limited to 'coqprime/README.md')
-rw-r--r--coqprime/README.md2
1 files changed, 1 insertions, 1 deletions
diff --git a/coqprime/README.md b/coqprime/README.md
index 8f1b93b12..9c317fb00 100644
--- a/coqprime/README.md
+++ b/coqprime/README.md
@@ -1,6 +1,6 @@
# 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.
+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