aboutsummaryrefslogtreecommitdiff
path: root/src/WeierstrassCurve/WeierstrassCurveTheorems.v
Commit message (Expand)AuthorAge
* rename-everythingGravatar Andres Erbsen2017-04-06
* note running time of Weierstrass associativity QedGravatar Andres Erbsen2017-04-06
* make elliptic curve proofs faster and split them into filesGravatar Andres Erbsen2017-04-05
* Set Suggest Proof Using seems to have been missing one?Gravatar Jason Gross2017-04-04
* Accurate Proof using for commutative_groupGravatar Jason Gross2017-04-04
* Fix WeierstrassCurveTheorems.vGravatar Jason Gross2017-04-04
* Add Proof using Type to WCT for faster "coqc" -quick -q -R "src" Crypto -R ...Gravatar Jason Gross2017-04-04
* Be more fine-grained in WeierstrassCurveTheorems importsGravatar Jason Gross2017-04-03
* make fsatz recurse when proving nonzero-ness, undo Weierstrass workaroundGravatar Andres Erbsen2017-03-30
* 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
* Weierstrass curve is a groupGravatar Andres Erbsen2017-03-02
* Attempt Weierstrass associativity again, good progress.Gravatar Andres Erbsen2017-03-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 16:46:22 +0000