aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Make Coq 8.5 the default target for Fiat-CryptoGravatar Jason Gross2016-06-22
* Handle renaming of NPeano.pow to Nat.pow (#3)Gravatar Jason Gross2016-06-22
* Add coq-scripts submodule for timing scriptsGravatar Jason Gross2016-06-22
* Also build with Coq 8.5 on travisGravatar Jason Gross2016-06-22
* EdDSA.v: resolve ambiguity based on ed25519.pyGravatar Andres Erbsen2016-06-21
* Whitespace changeGravatar Jason Gross2016-06-21
* Fix a missing mod resolutionGravatar Jason Gross2016-06-21
* NPeano.modulo became Nat.modulo in 8.5Gravatar Jason Gross2016-06-21
* Import omega for 8.5Gravatar Jason Gross2016-06-21
* Shadowing of ltac constr-bound variables with identifiers is forbidden in 8.5Gravatar Jason Gross2016-06-21
* Use Admitted, not Qed, when a proof has admitGravatar Jason Gross2016-06-21
* Fix [Proper_add] in 8.5Gravatar Jason Gross2016-06-21
* Make [bash] tactic easier to debugGravatar Jason Gross2016-06-21
* use Local Obligation Tactic (8.5-compat)Gravatar Andres Erbsen2016-06-21
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
* Algebra: change a aliasing definition into an aliasing lemma to appease impli...Gravatar Andres Erbsen2016-06-20
* parenthesize Ltac [constr:] argumentsGravatar Andres Erbsen2016-06-20
* Fix nsatz_compute for 8.4Gravatar Jason Gross2016-06-20
* Add travis build status indicatorGravatar Jason Gross2016-06-20
* 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
* Add .travis.ymlGravatar Jason Gross2016-06-20
* Fix for Coq 8.4pl2Gravatar Jason Gross2016-06-20
* readme typoGravatar Andres Erbsen2016-06-20
* move nsatz into tactics directoryGravatar Andres Erbsen2016-06-20
* readme: dont say things I am not sure ofGravatar 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
|\
* | Makefile: build on Arch Linux once againGravatar 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
* | Fix .mailmap (correct name on the left)Gravatar Jason Gross2016-06-18
* | Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-06-17
|\ \
* | | 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
| * | Be a bit more quiet on make unless VERBOSE=1 is passedGravatar Jason Gross2016-06-16
| | * 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 04:44:51 +0000