aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* Revert "Add -compat 8.6 to _CoqProject"Gravatar Jason Gross2017-10-18
* Add InterpRewritingGravatar Jason Gross2017-10-17
* Add CacheTermGravatar Jason Gross2017-10-17
* Add MulSplitUnfolderGravatar Jason Gross2017-10-17
* Add faster arithmetic unfoldingGravatar Jason Gross2017-10-15
* Add TagListGravatar Jason Gross2017-10-10
* Add UniformWeightInstancesGravatar Jason Gross2017-10-09
* Factor out parameter-specific codeGravatar Jason Gross2017-10-07
* Add PoseTermWithNameGravatar Jason Gross2017-10-05
* Add some ZUtil lemmasGravatar Jason Gross2017-10-03
* Add missing fileGravatar Jason Gross2017-09-21
* Add femul,fesqure for C32Gravatar Jason Gross2017-09-21
* Split off tactics in IntegrationTestDisplayCommonGravatar Jason Gross2017-09-21
* Add UnfoldArgGravatar Jason Gross2017-07-08
* automate P256 integrationGravatar Andres Erbsen2017-07-02
* Reorganization of saturated arithmeticGravatar jadep2017-06-29
* Add nonzero synthesisGravatar Jason Gross2017-06-26
* Weierstrass Jacobian mixed additionGravatar Andres Erbsen2017-06-23
* Add (partially admitted) integration tests for add, sub, oppGravatar Jason Gross2017-06-22
* move Specifi p256 files into their own directoryGravatar Andres Erbsen2017-06-22
* src/Demo.v: a 200-line introduction to BaseSystem ideasGravatar Andres Erbsen2017-06-21
* Add fold_left_orb_true, fold_left_orb_pullGravatar Jason Gross2017-06-20
* Add ModInvGravatar Jason Gross2017-06-18
* compile X25519 C code from MakefileGravatar Andres Erbsen2017-06-18
* add 128-bit display fileGravatar Jason Gross2017-06-17
* Add 128-bit version of montgomery for testingGravatar Jason Gross2017-06-17
* Finish MontgomeryP256 (less conditional subtract)Gravatar Jason Gross2017-06-17
* Add initial IntegrationTestMontgomeryP256.vGravatar Jason Gross2017-06-17
* Fix spellingGravatar Jason Gross2017-06-17
* Switch to using tuples for word-by-word montgomeryGravatar Jason Gross2017-06-16
* Fix buildGravatar Jason Gross2017-06-16
* Revert PR #203Gravatar Jason Gross2017-06-16
* Revert "Revert "Add CArrayNotations""Gravatar Jason Gross2017-06-16
* Revert "Add CArrayNotations"Gravatar Jason Gross2017-06-15
* Finish karatsuba mul, add display file (#199)Gravatar Jason Gross2017-06-15
* Add CArrayNotationsGravatar Jason Gross2017-06-15
* Add -compat 8.6 to _CoqProjectGravatar Jason Gross2017-06-15
* Add ZUtil.Z2NatGravatar Jason Gross2017-06-15
* Edwards coordinates precomputed addition formulaGravatar Andres Erbsen2017-06-15
* move CPS notations to Util.CPSNotationsGravatar Andres Erbsen2017-06-15
* ScalarMult: Z -> G -> G (closes #193)Gravatar Andres Erbsen2017-06-14
* Stronger invert_op tacticGravatar Jason Gross2017-06-13
* Add Z.peano_rectGravatar Jason Gross2017-06-13
* Add Z.mul_splitGravatar Jason Gross2017-06-13
* WBW-montgomery: Fill in most context variablesGravatar Jason Gross2017-06-13
* Add CompileInterpSideConditions.vGravatar Jason Gross2017-06-12
* Add snd_interpf_side_conditions_gen_SomeGravatar Jason Gross2017-06-12
* Add Named.InterpSideConditionsGravatar Jason Gross2017-06-12
* Add Z.InterpSideConditionsGravatar Jason Gross2017-06-12
* Add InterpSideConditionsGravatar Jason Gross2017-06-12