aboutsummaryrefslogtreecommitdiff
path: root/src/Spec/CompleteEdwardsCurve.v
Commit message (Expand)AuthorAge
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Strip trailing whitespaceGravatar Jason Gross2017-06-02
* rename-everythingGravatar Andres Erbsen2017-04-06
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* WIPGravatar Andres Erbsen2017-03-02
* address some code review commentsGravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* fsatz, nsatz_solve_nonzeroGravatar Andres Erbsen2017-03-02
* use field_nsatz in CompleteEdwardsCurve.PreGravatar Andres Erbsen2017-03-02
* remove eq_dec from MonoidGravatar Andres Erbsen2016-08-23
* remove field_algebraGravatar Andres Erbsen2016-07-11
* Fix broken notations (hopefully)Gravatar Jason Gross2016-06-22
* use Local Obligation Tactic (8.5-compat)Gravatar Andres Erbsen2016-06-21
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
* move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheoremsGravatar Andres Erbsen2016-06-17
* port edwards curve specGravatar Andres Erbsen2016-06-16
* consolidate and rename Edwards curve lemmasGravatar Andres Erbsen2016-04-25
* point_eq_decGravatar Andres Erbsen2016-04-22
* nicer verify() derivation starterGravatar Andres Erbsen2016-03-21
* Finish absolutizing importsGravatar Jason Gross2016-03-10
* document field issue re-appearingGravatar Andres Erbsen2016-02-12
* port some edwards curve theoremsGravatar Andres Erbsen2016-02-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 19:18:34 +0000