aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Set Asymmetric Patterns, add util lemmas about sigGravatar Jason Gross2016-07-29
* Get rid of unparsable unicode notationGravatar Jason Gross2016-07-28
* Add more reserved notationsGravatar Jason Gross2016-07-28
* Add instances about congruence moduloGravatar Jason Gross2016-07-28
* Add unicode reserved notationsGravatar Jason Gross2016-07-28
* Add Z.mod_mod to zsimplifyGravatar Jason Gross2016-07-28
* Move most notation level declarations into UtilGravatar Jason Gross2016-07-27
* Restore functionality of Z.simplify_fractions_leGravatar Jason Gross2016-07-27
* Make Z.pre_reorder_fractions / Z.simplify_fractions_le not loopGravatar Jason Gross2016-07-27
* Add another ZUtil lemmaGravatar Jason Gross2016-07-26
* Fix 8.6 buildGravatar Jason Gross2016-07-26
* Fix 8.4 build.Gravatar jadep2016-07-25
* Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-25
|\
* | Put ModularBaseSystem carries in terms of [carry_gen], and pushed this change...Gravatar jadep2016-07-25
* | A couple new util lemmasGravatar jadep2016-07-25
| * More Zpow in ZUtilGravatar Jason Gross2016-07-22
| * More ZUtilGravatar Jason Gross2016-07-22
| * Add databases for ring_simplifyGravatar Jason Gross2016-07-22
| * Add reverse_nondep and ring_simplify_subterms_in_all tacticsGravatar Jason Gross2016-07-22
| * More ZUtil lemmasGravatar Jason Gross2016-07-22
| * Revert "Revert "Add more ZUtil automation""Gravatar Jason Gross2016-07-22
| * Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
| * Revert "Add more ZUtil automation"Gravatar Jason Gross2016-07-22
| * Add more ZUtil automationGravatar Jason Gross2016-07-22
| * Add ring_simplify_subtermsGravatar Jason Gross2016-07-22
| * Generalize div_sub_small a bitGravatar Jason Gross2016-07-22
|/
* 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
| * Add ZUtil lemmasGravatar Jason Gross2016-07-21
|/
* Removed lingering print statement.Gravatar jadep2016-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
| * 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
* | 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