# 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