aboutsummaryrefslogtreecommitdiff
path: root/src/CompleteEdwardsCurve/ExtendedCoordinates.v
Commit message (Expand)AuthorAge
* Move most notation level declarations into UtilGravatar Jason Gross2016-07-27
* Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
* proved an admit in field homomorphisms that turned out to be unprovable; I ad...Gravatar jadep2016-07-15
* remove field_algebraGravatar Andres Erbsen2016-07-11
* wrap nsatz in AlgebraGravatar Andres Erbsen2016-07-11
* ExtendedCoordinates: group.Gravatar Andres Erbsen2016-06-24
* Fix broken notations (hopefully)Gravatar Jason Gross2016-06-22
* Aggregate all level specifications not in Spec/*Gravatar Jason Gross2016-06-22
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
* move nsatz into tactics directoryGravatar Andres Erbsen2016-06-20
* tuple toolingGravatar Andres Erbsen2016-06-20
* port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...Gravatar Andres Erbsen2016-06-18
* ERep addGravatar Andres Erbsen2016-05-29
* before changing SRep from N to F lGravatar Andres Erbsen2016-05-27
* slightly nicer edwards curve extended coordinates additionGravatar Andres Erbsen2016-05-18
* ed25519: solve elliptic curve math admitsGravatar Andres Erbsen2016-04-25
* consolidate and rename Edwards curve lemmasGravatar Andres Erbsen2016-04-25
* Add a tactic for field inequalitiesGravatar Jason Gross2016-04-19
* Retrieved updated version of Util/IterAssocOp and modified ExtendedCoordinate...Gravatar jadep2016-04-14
* extended coordinates setoid boilerplateGravatar Andres Erbsen2016-03-20
* ModularArithmetic: [field] tactic that respects opacity, prettify ExtendedCoo...Gravatar Andres Erbsen2016-02-28
* CompleteEdwardsCurve: unifiedAddM1: Closed Under Global ContextGravatar Andres Erbsen2016-02-15
* document field issue re-appearingGravatar Andres Erbsen2016-02-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 23:18:31 +0000