aboutsummaryrefslogtreecommitdiff
path: root/src/CompleteEdwardsCurve/Pre.v
Commit message (Expand)AuthorAge
* proved an admit in field homomorphisms that turned out to be unprovable; I ad...Gravatar jadep2016-07-15
* s/conservative_common_denominator/common_denominator/gGravatar Andres Erbsen2016-07-11
* remove field_algebraGravatar Andres Erbsen2016-07-11
* wrap nsatz in AlgebraGravatar Andres Erbsen2016-07-11
* update new lemma in CompleteEdwardsCurve/Pre to match other changes to that fileGravatar jadep2016-06-25
* Merge branch 'master' of github.com:mit-plv/fiat-crypto into pointencoding_portGravatar jadep2016-06-24
|\
* \ merging point encoding portGravatar jadep2016-06-24
|\ \
* | | Ported PointEncodings to parameterize over field rather than modulus.Gravatar jadep2016-06-24
| | * Remove a useless introGravatar Jason Gross2016-06-24
| |/
| * Integrate Pseudize into Pipeline.vGravatar Robert Sloan2016-06-23
| * Pseudize Let_InGravatar Robert Sloan2016-06-23
| * 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
| * port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...Gravatar Andres Erbsen2016-06-18
| * edwards curve addition respects field homomorphismGravatar 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
| * refactor nsatz wrappers into algebra fileGravatar Andres Erbsen2016-06-14
| * [field] and [nsatz] do things now againGravatar Andres Erbsen2016-06-14
| * stuck because overloading-by-typeclasses sucksGravatar Andres Erbsen2016-06-13
* | Minor 8.5 changesGravatar Jason Gross2016-06-10
* | More changes for 8.5Gravatar Jason Gross2016-06-10
| * generic field definitionGravatar Andres Erbsen2016-06-07
|/
* Finish absolutizing importsGravatar Jason Gross2016-03-10
* port some edwards curve theoremsGravatar Andres Erbsen2016-02-12