aboutsummaryrefslogtreecommitdiff
path: root/coqprime
Commit message (Expand)AuthorAge
* Absolutize Coqprime importsGravatar Jason Gross2016-06-22
* Automate a UList proof a bit so it builds with 8.5Gravatar Jason Gross2016-06-22
* Update Coqprime/UListGravatar Jason Gross2016-06-22
* Update build process to use COQPATH & _CoqProjectGravatar Jason Gross2016-06-22
* EdDSA25519 : wrote and proved optimized PointEncoding, which encodes y and th...Gravatar Jade Philipoom2016-06-22
* Import coqprime; use it to prove Euler's criterion.Gravatar Jade Philipoom2016-06-22