aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/SC25519.v
Commit message (Collapse)AuthorAge
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
|
* Work around bug #5198 (broken tc resolution)Gravatar Jason Gross2016-11-12
| | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=5198, Inlining lets breaks typechecking of [Definition]s
* Fix out of memory error for 8.5,8.5pl1Gravatar Jason Gross2016-10-19
|
* Fix for Coq 8.4 evar propogationGravatar Jason Gross2016-10-18
|
* Fix missing importsGravatar Jason Gross2016-10-17
|
* Remove broken importsGravatar Jason Gross2016-10-17
|
* Rename and clean up exponent codeGravatar Jason Gross2016-10-17