aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* More missing scopes for 8.5?Gravatar Jason Gross2016-06-20
* More 8.5 fixesGravatar Jason Gross2016-06-20
* Variosu 8.5 fixesGravatar Jason Gross2016-06-20
* Fix for Coq 8.4pl2Gravatar Jason Gross2016-06-20
* move nsatz into tactics directoryGravatar Andres Erbsen2016-06-20
* remove obsolete rep mechanismGravatar Andres Erbsen2016-06-20
* GF25519: quietGravatar Andres Erbsen2016-06-20
* Remove anything incompatible with new algebraic hierarcyGravatar Andres Erbsen2016-06-20
* Merge branch 'field-experiment'Gravatar Andres Erbsen2016-06-20
|\
| * [F q] is [Algebra.field]Gravatar Andres Erbsen2016-06-20
| * port EdDSA specGravatar Andres Erbsen2016-06-20
| * tuple toolingGravatar Andres Erbsen2016-06-20
| * port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...Gravatar Andres Erbsen2016-06-18
* | Canonicalization is now automated in GF25519 and added to GF1305.Gravatar jadep2016-06-17
* | Specific version of freeze for GF25519 (automation still needs a little work)Gravatar jadep2016-06-17
| * move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheoremsGravatar Andres Erbsen2016-06-17
| * Z is integral domainGravatar Andres Erbsen2016-06-16
| * port edwards curve specGravatar Andres Erbsen2016-06-16
| * edwards curve addition respects field homomorphismGravatar Andres Erbsen2016-06-16
| * algebra: add homomorphismsGravatar Andres Erbsen2016-06-16
| * prove ring admitsGravatar Andres Erbsen2016-06-16
| * edwards curve preliminaries: replace oncurve proof with nsatzGravatar Andres Erbsen2016-06-16
| * nsatz: reimplement, integrate, demonstrateGravatar Andres Erbsen2016-06-15
* | PseudoMersenneBaseRep.mul now carries by default (made possible by strictly b...Gravatar jadep2016-06-15
* | changed representation definition to require digits vector to be the exact le...Gravatar jadep2016-06-15
* | Added canonicalization to ModularBaseSystemOpt.Gravatar jadep2016-06-15
* | MergeGravatar jadep2016-06-14
|\ \
* | | Finished admits for canonicalization proofs.Gravatar jadep2016-06-14
| | * refactor nsatz wrappers into algebra fileGravatar Andres Erbsen2016-06-14
| | * [field] and [nsatz] do things now againGravatar Andres Erbsen2016-06-14
* | | reversed modulus_digits and proved a few admitsGravatar jadep2016-06-13
* | | progress on second stage (conditional constant-time subtraction) of canonical...Gravatar jadep2016-06-13
| | * stuck because overloading-by-typeclasses sucksGravatar Andres Erbsen2016-06-13
| | * indentGravatar Andres Erbsen2016-06-12
| * | Another fix for an anomaly in 8.4pl2Gravatar Jason Gross2016-06-11
| * | More Coq 8.4pl2 fixesGravatar Jason Gross2016-06-11
| * | Fix for Coq 8.4pl2Gravatar Jason Gross2016-06-11
| * | Work around bug #4811 (slow f_equal)Gravatar Jason Gross2016-06-11
* | | starting rewrite using different definition of mapGravatar jadep2016-06-11
| * | Minor 8.5 changesGravatar Jason Gross2016-06-10
| * | More changes for 8.5Gravatar Jason Gross2016-06-10
| * | 8.5 fixesGravatar Jason Gross2016-06-10
|/ /
| * improved generic field libraryGravatar Andres Erbsen2016-06-10
| * improve generic field libraryGravatar Andres Erbsen2016-06-10
| * experimentGravatar Andres Erbsen2016-06-07
| * generic field definitionGravatar Andres Erbsen2016-06-07
| * ed25519: refactor some ProperGravatar Andres Erbsen2016-06-06
| * rewrite in Let_In binder by tacticGravatar Andres Erbsen2016-06-04
| * Let_In rewritingGravatar Andres Erbsen2016-06-03
| * leibniz equal version of topdown rewriting of sigma types: nicerGravatar Andres Erbsen2016-06-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 20:44:41 +0000