aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments
Commit message (Expand)AuthorAge
* Move most notation level declarations into UtilGravatar Jason Gross2016-07-27
* Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
* ed25519 spec: small cleanupGravatar Andres Erbsen2016-07-21
* compute on [F q]!Gravatar Andres Erbsen2016-07-20
* experiments wd25519: simplify proof for aGravatar Andres Erbsen2016-07-20
* Silence a warningGravatar Jason Gross2016-07-18
* Remove a nested proofGravatar Jason Gross2016-07-18
* ported IterAssocOp to use monoid rather than a billion context variables that...Gravatar jadep2016-07-18
* Experiments/SpecificCurve25519.v: curve25519 addition using small Z-sGravatar Andres Erbsen2016-07-13
* Merge of fixedlength and masterGravatar jadep2016-07-11
|\
| * added proofs about addition chain exponentiation for later use in ModularBase...Gravatar jadep2016-07-10
* | stuck trying to figure out dependently typed continuation passing styleGravatar Andres Erbsen2016-07-06
|/
* EdDSARefinement: work around rewrite_strat for 8.4Gravatar Andres Erbsen2016-06-28
* eddsa refinement setupGravatar Andres Erbsen2016-06-27
* scalarmult support; EdDSA.sign produces valid signaturesGravatar Andres Erbsen2016-06-27
* first pass of scalarmultGravatar Andres Erbsen2016-06-27
* Fix for Coq 8.4Gravatar Jason Gross2016-06-25
* EdDSA: prove things about specGravatar Andres Erbsen2016-06-25
* Fix a missing mod resolutionGravatar Jason Gross2016-06-21
* NPeano.modulo became Nat.modulo in 8.5Gravatar Jason Gross2016-06-21
* Import omega for 8.5Gravatar Jason Gross2016-06-21
* Shadowing of ltac constr-bound variables with identifiers is forbidden in 8.5Gravatar Jason Gross2016-06-21
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
* Variosu 8.5 fixesGravatar Jason Gross2016-06-20
* remove obsolete rep mechanismGravatar Andres Erbsen2016-06-20
* Remove anything incompatible with new algebraic hierarcyGravatar Andres Erbsen2016-06-20
* Merge branch 'field-experiment'Gravatar Andres Erbsen2016-06-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 16:38:52 +0000