aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* 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
* 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
* 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
* 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 curve25519-donna-c64 to etc/third_partyGravatar Jason Gross2017-09-27
* Add missing fileGravatar Jason Gross2017-09-21
* Add femul,fesqure for C32Gravatar Jason Gross2017-09-21
* Update constants filesGravatar Jason Gross2017-09-21
* Add extract_ExprGravatar Jason Gross2017-09-21
* Split off tactics in IntegrationTestDisplayCommonGravatar Jason Gross2017-09-21
* make benchGravatar Jason Gross2017-09-12
* fsatz tests: 1/(1/x) = xGravatar Andres Erbsen2017-09-11
* Fix more commented out alternativesGravatar Jason Gross2017-09-05
* Fix commented out alternate version in ladderstepGravatar Jason Gross2017-09-05
* Add decidable equality with nilGravatar Jason Gross2017-08-13
* Factor out some of the preglue synthesis codeGravatar Jason Gross2017-07-08
* Unfold tuple arguments in reflective pipelineGravatar Jason Gross2017-07-08
* Add cbv_runtime in Arithmetic/CoreGravatar Jason Gross2017-07-08
* Make some tactics a bit more powerfulGravatar Jason Gross2017-07-08
* Fix Demo.vGravatar Jason Gross2017-07-08
* More fine-grained tactics importsGravatar Jason Gross2017-07-08
* More fine-grained importsGravatar Jason Gross2017-07-08
* Add UnfoldArgGravatar Jason Gross2017-07-08
* Fix CSE_sym denoteGravatar Jason Gross2017-07-07
* Fix proofs broken by previous commitGravatar Jason Gross2017-07-07
* Stronger contextsGravatar Jason Gross2017-07-07
* Remove some admitted lemmasGravatar Jason Gross2017-07-07
* enforce use of [F.zero], [F.one]; prove Ed25519 admitsGravatar Andres Erbsen2017-07-07
* prove ModularArithmeticTheorems admitsGravatar Andres Erbsen2017-07-06
* Curves/Edwards/Affine: prove point compression admitsGravatar Andres Erbsen2017-07-06
* prove an admit in ArithmeticSynthesisTestGravatar Andres Erbsen2017-07-06
* make benchGravatar Andres Erbsen2017-07-06
* make benchGravatar Jason Gross2017-07-06
* Fix a typo that ends up not matteringGravatar Jason Gross2017-07-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 18:58:21 +0000