aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
* Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-21
|\
* | Fix 8.4{pl1,pl2} buildsGravatar jadep2016-07-21
| * Add another lemma to zarithGravatar Jason Gross2016-07-21
* | Changed name of [carry_and_reduce_single] to [carry_single], since it does no...Gravatar jadep2016-07-21
| * Split up proof in BarrettReduction.ZGravatar Jason Gross2016-07-21
| * Add another ZUtil lemmaGravatar Jason Gross2016-07-21
| * Another ZUtil lemmaGravatar Jason Gross2016-07-21
| * Fix broken proofsGravatar Jason Gross2016-07-21
| * Add more ZUtilGravatar Jason Gross2016-07-21
| * More ZUtil helper lemmasGravatar Jason Gross2016-07-21
| * Add more ZUtil lemmasGravatar Jason Gross2016-07-21
| * Update .mailmapGravatar Jason Gross2016-07-21
| * Add ZUtil lemmasGravatar Jason Gross2016-07-21
|/
* Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-21
|\
* | Removed lingering print statement.Gravatar jadep2016-07-21
| * Faster update-_CoqProject targetGravatar Jason Gross2016-07-21
| * Fix clean targetGravatar Jason Gross2016-07-21
* | Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-21
|\|
* | Fixes #29Gravatar jadep2016-07-21
* | re-introduced extra field isomorphism layer for 8.4 compatibility and better ...Gravatar jadep2016-07-21
| * ed25519 spec: small cleanupGravatar Andres Erbsen2016-07-21
| * Add support for TIMED=1 in Coq 8.4Gravatar Jason Gross2016-07-20
| * Don't depend on the submodule; copy-paste insteadGravatar Jason Gross2016-07-20
| * Add a separate non-specific targetGravatar Jason Gross2016-07-20
| * Merge pull request #33 from JasonGross/dir-localsGravatar Andres Erbsen2016-07-20
| |\
| * | automate a proofGravatar Andres Erbsen2016-07-20
| * | compute on [F q]!Gravatar Andres Erbsen2016-07-20
| * | experiments wd25519: simplify proof for aGravatar Andres Erbsen2016-07-20
| | * Add target for .dir-locals.elGravatar Jason Gross2016-07-20
| |/
* | Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-20
|\|
* | mergeGravatar jadep2016-07-20
|\ \
| | * Move mul_rep_extended (do we actually care about this?)Gravatar Jason Gross2016-07-20
| |/
| * Don't use auto with *Gravatar Jason Gross2016-07-20
* | restructured ModularBaseSystem pipeline to put tuple conversion before Modula...Gravatar jadep2016-07-20
| * Absolutize some importsGravatar Jason Gross2016-07-20
| * Silence a deprecation warningGravatar Jason Gross2016-07-20
| * Display pretty timing graph on travisGravatar Jason Gross2016-07-20
| * Remove dependency of ext_base on pseudomersenneGravatar Jason Gross2016-07-20
| * Add Z.lt_le_incl to zarithGravatar Jason Gross2016-07-20
| * Add another lemma about +, <= to arithGravatar Jason Gross2016-07-20
| * Use a proof that doesn't require as many assumptions in extended_base_lengthGravatar Jason Gross2016-07-20
| * Work around bad design in CoqGravatar Jason Gross2016-07-19
| * Add a distr_length databaseGravatar Jason Gross2016-07-19
| * Remove stuff from PseudoMersenneBaseParamProofs.vGravatar Jason Gross2016-07-19
| * {base} -> baseGravatar Jason Gross2016-07-19
| * Move two_k_nonzero to PseudoMersenneBaseParamProofs.vGravatar Jason Gross2016-07-19
| * Fix side-condition from previous commitGravatar Jason Gross2016-07-19
| * Add another lemma to distr_lengthGravatar Jason Gross2016-07-19
* | mergeGravatar jadep2016-07-19
|\|
* | Converted non-canonicalization sections of ModularBaseSystemProofs to tuples.Gravatar jadep2016-07-19