aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
* More map -> List.mapGravatar Jason Gross2016-09-29
* map -> List.map (not Tuple.map)Gravatar Jason Gross2016-09-29
* Add Tuple.mapGravatar Jason Gross2016-09-29
* Small example of bounds-calculation with dependent types (#61)Gravatar Jason Gross2016-09-29
* montgomery-curveGravatar Andres Erbsen2016-09-28
* Merge pull request #69 from JasonGross/scalable-scalarsGravatar Jason Gross2016-09-26
|\
| * Add a comment with an exampleGravatar Jason Gross2016-09-26
* | MxDH: do not depend on implicit import of list notationsGravatar Andres Erbsen2016-09-26
* | add Montgomery x-coordinate Diffie-Hellman and Curve25519Gravatar Andres Erbsen2016-09-26
* | Finished remaining admits in [freeze] proofsGravatar jadep2016-09-23
| * Drop CSE from Fancy MachineGravatar Jason Gross2016-09-22
| * Use dlet, not lletGravatar Jason Gross2016-09-22
| * Fix for Coq < 8.6Gravatar Jason Gross2016-09-22
| * Don't inline everything in Montgomery and BarrettGravatar Jason Gross2016-09-22
| * Make use of named syntax, do reg assign for fancyGravatar Jason Gross2016-09-22
| * Add dead code eliminationGravatar Jason Gross2016-09-22
| * Add a non-higher-order syntax, and reg assignmentGravatar Jason Gross2016-09-22
|/
* Revert "Add a locked version of [let] with fewer reductions"Gravatar Jason Gross2016-09-22
* Revert "Update _CoqProject"Gravatar Jason Gross2016-09-22
* Revert "Fix LockedLet"Gravatar Jason Gross2016-09-22
* Fix a typoGravatar Jason Gross2016-09-22
* Add a form of Let_In that carries a proofGravatar Jason Gross2016-09-22
* move eddsa rep changeGravatar Andres Erbsen2016-09-22
* alternative signing derivationGravatar Andres Erbsen2016-09-22
* Util.LetIn: fix proper instanceGravatar Andres Erbsen2016-09-22
* Fix LockedLetGravatar Jason Gross2016-09-22
* Update _CoqProjectGravatar Jason Gross2016-09-22
* Add a locked version of [let] with fewer reductionsGravatar Jason Gross2016-09-22
* Generalize count_letsGravatar Jason Gross2016-09-21
* Deduplicate codeGravatar Jason Gross2016-09-21
* Add some util files for reflective let bindingsGravatar Jason Gross2016-09-21
* Reorganization, moving of lemmas to correct files, and 8.4 compatibilityGravatar jadep2016-09-21
* Proved specification of constant-time modulus comparison (except for one ZUti...Gravatar jadep2016-09-21
* Generalize InlineConstGravatar Jason Gross2016-09-20
* Allow passing PROFILE=1 to make for -profile-ltacGravatar Jason Gross2016-09-20
* Change [Let ... in ...] to [dlet ... in ...] (#67)Gravatar Jason Gross2016-09-19
* Make the example a function for reificationGravatar Jason Gross2016-09-18
* Add dec eq for option, listGravatar Jason Gross2016-09-18
* Better arguments for SmartVarMapGravatar Jason Gross2016-09-18
* Arguments for SmartVarMapGravatar Jason Gross2016-09-18
* Generalize SmartVarVarGravatar Jason Gross2016-09-18
* Fix the 8.4 build by changing a couple standard library namesGravatar jadep2016-09-18
* Util.Notations: change Let to match slet\Gravatar Andres Erbsen2016-09-18
* Add reserved notation for Let, change #Gravatar Jason Gross2016-09-17
* Move side lemmas to appropriate filesGravatar jadep2016-09-17
* Partially flesh out [freeze] proofs; also parameterize [sqrt_5mod8] over impl...Gravatar jadep2016-09-17
* Proved bounds for [encode] results; fleshed out some structure for [freeze] p...Gravatar jadep2016-09-17
* Fix missing parenthesisGravatar jadep2016-09-17
* Remove unused lemma and standardized use of notations for [freeze] proofsGravatar jadep2016-09-17
* deduplicate Let_In into src/Util/LetIn.vGravatar Andres Erbsen2016-09-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-20 04:28:44 +0000