aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Update smithers scriptGravatar Jason Gross2017-10-13
* add primes list andres scraped from curves at moderncrypto dot orgGravatar jadep2017-10-13
* add file input/output to json-generating scriptGravatar jadep2017-10-13
* add support for unsaturated limbs in json-generationGravatar jadep2017-10-13
* add examples to json-generation file for referenceGravatar jadep2017-10-13
* add script to generate json files given a primeGravatar jadep2017-10-13
* Add some SmartMap tuple lemmasGravatar Jason Gross2017-10-13
* Fix a spelling errorGravatar Jason Gross2017-10-13
* Factor out truncation_boundsGravatar Jason Gross2017-10-13
* Add comment to Compilers/Z/Bounds/Interpretation.vGravatar Jason Gross2017-10-13
* Add some helper compilation lemmasGravatar Jason Gross2017-10-13
* Add reflective compose, notation for Z.Syntax.{Expr,Interp}Gravatar Jason Gross2017-10-12
* Allow test and bench to fail on travisGravatar Jason Gross2017-10-11
* Add targets for no-curves-proofs-non-specific, and selected-specific,Gravatar Jason Gross2017-10-11
* Smithers doesn't support -o pipefailGravatar Jason Gross2017-10-11
* Factor out -w "-notation-overridden" in MakefileGravatar Jason Gross2017-10-10
* Add etc/ci/smithers.sh for smithers testingGravatar Jason Gross2017-10-10
* More Makefile factoringGravatar Jason Gross2017-10-10
* Update Makefile by deduplicating some file listsGravatar Jason Gross2017-10-10
* Hopefully fix travisGravatar Jason Gross2017-10-10
* Add update_by_tac_if_not_existsGravatar Jason Gross2017-10-10
* TagList: make get error, and fix bugsGravatar Jason Gross2017-10-10
* Add TagListGravatar Jason Gross2017-10-10
* Add notationsGravatar Jason Gross2017-10-10
* Add UniformWeightInstancesGravatar Jason Gross2017-10-09
* Fix .dir-locals.el to work on WindowsGravatar Jason Gross2017-10-07
* Generalize phisGravatar Jason Gross2017-10-07
* Factor out the compute bit of the compute notation in curve paramsGravatar Jason Gross2017-10-07
* Factor out parameter-specific codeGravatar Jason Gross2017-10-07
* [travis] trunk is now called masterGravatar Jason Gross2017-10-06
* Switch Coq {8.6 => 8.6.1} on travisGravatar Jason Gross2017-10-06
* Drop 8.5 travis buildGravatar Jason Gross2017-10-06
* Fix printenv sed script in Makefile for Windows supportGravatar Jason Gross2017-10-06
* Coq 8.5 can't handle symbol-free notationsGravatar Jason Gross2017-10-06
* Fix display logGravatar Jason Gross2017-10-06
* Clean up TestCase a bitGravatar Jason Gross2017-10-06
* Add another constantGravatar Jason Gross2017-10-06
* Fix the printlite targetGravatar Jason Gross2017-10-06
* Add pow_ceil_mul_nat_nonnegGravatar Jason Gross2017-10-05
* Add PoseTermWithNameGravatar Jason Gross2017-10-05
* Factor out some bits of ladderstep preglueGravatar Jason Gross2017-10-05
* Add some ZUtil lemmasGravatar Jason Gross2017-10-03
* Make some typeclasses opaqueGravatar Jason Gross2017-10-02
* Speed up reification a little bitGravatar Jason Gross2017-10-02
* Add missing tactic in comment in ladderstepGravatar Jason Gross2017-09-27
* Add src/Specific/X25519/C32/compiler.sh, update src/Specific/X25519/C64/scala...Gravatar Jason Gross2017-09-27
* Add BITWIDTH=64 to extract-function.sh rule in MakefileGravatar Jason Gross2017-09-27
* Add example usageGravatar Jason Gross2017-09-27
* Update etc scripts to include governorGravatar Jason Gross2017-09-27
* Add curve25519-donna-c64 to etc/third_partyGravatar Jason Gross2017-09-27