aboutsummaryrefslogtreecommitdiff
path: root/coqprime
Commit message (Collapse)AuthorAge
* Absolutize Coqprime importsGravatar Jason Gross2016-06-22
| | | | | | | | | | Used ```bash cd coqprime make -kj10 cd Coqprime git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Coqprime ```
* Automate a UList proof a bit so it builds with 8.5Gravatar Jason Gross2016-06-22
| | | | It still builds with 8.4
* Update Coqprime/UListGravatar Jason Gross2016-06-22
| | | | | Ambiguous imports, oh joy! (Coqprime failed to build when Bedrock was in COQPATH.)
* Update build process to use COQPATH & _CoqProjectGravatar Jason Gross2016-06-22
| | | | | | | | Removed all of the files not built by default; they can be resurrected from git history. _CoqProject is the standard way to list the files in a project and to give information to coq_makefile. COQPATH is the standard way to make use of not-yet-installed libraries that are not part of your project (i.e., you don't want to remove them when you `make clean`, etc.).
* EdDSA25519 : wrote and proved optimized PointEncoding, which encodes y and ↵Gravatar Jade Philipoom2016-06-22
| | | | | | the sign bit of x, then solves the curve equation for x ^ 2. Required adding several lemmas to GaloisField (and moving others there from PointFormats). recursive-build coqprime
* Import coqprime; use it to prove Euler's criterion.Gravatar Jade Philipoom2016-06-22