aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* Add WfInversionGravatar Jason Gross2016-12-03
* Move things to ExprInversionGravatar Jason Gross2016-12-03
* Initial (not fully working) version of MapWithInterpInfoGravatar Jason Gross2016-12-02
* Add lemmas about applicationGravatar Jason Gross2016-11-22
* Copy bounds, fix a typoGravatar Jason Gross2016-11-22
* Add GF25519BoundedExtendedAddCoordinatesGravatar Jason Gross2016-11-17
* Add src/Specific/GF25519BoundedAddCoordinates.vGravatar Jason Gross2016-11-17
* Add ReflectiveAddCoordinatesGravatar Jason Gross2016-11-17
* Add some missing filesGravatar Jason Gross2016-11-17
* Update AddCoordinatesGravatar Jason Gross2016-11-17
* Move util definitions to util folderGravatar Jason Gross2016-11-17
* Copy reified add coordinates to various versions of curvesGravatar Jason Gross2016-11-17
* Add reified mostly-bounds-checked add_coordinatesGravatar Jason Gross2016-11-17
* Update field names in SpecificGenGravatar Jason Gross2016-11-17
* Move ExtendedAddCoordinates to new file, SpecGenGravatar Jason Gross2016-11-17
* Support for 128-bit wordsGravatar Jason Gross2016-11-14
* Add word-size-independent interpretationsGravatar Jason Gross2016-11-14
* Add SpecificGen/GF*Gravatar Jason Gross2016-11-13
* make update-_CoqProjectGravatar Jason Gross2016-11-11
* Don't build autogenerated files for nowGravatar jadep2016-11-11
* Automatically generate code for field operations with different primesGravatar jadep2016-11-11
* Freeze stubsGravatar Jason Gross2016-11-11
* Split up GF25519Reflective.Common: faster+parallelGravatar Jason Gross2016-11-09
* Factor related_Z_op (except conditional_sub)Gravatar Jason Gross2016-11-08
* Add IffT, some Proper prod lemmasGravatar Jason Gross2016-11-07
* implement X25519Gravatar Andres Erbsen2016-11-06
* Split off some things from InterpretationsGravatar Jason Gross2016-11-05
* separate Ed25519Extraction.v, add extraction to MakefileGravatar Andres Erbsen2016-11-03
* Move hlist to new fileGravatar Jason Gross2016-11-01
* Add Reflection.ApplicationGravatar Jason Gross2016-10-31
* Switch to reflective bounded word in Ed25519Gravatar Jason Gross2016-10-31
* Add src/Specific/GF25519Reflective.vGravatar Jason Gross2016-10-31
* Switch to a faster way of proving wfGravatar Jason Gross2016-10-30
* Add PartiallyReifiedPropGravatar Jason Gross2016-10-30
* Add reification of various operationsGravatar Jason Gross2016-10-30
* Add initial work on reifying GF25519 stuffGravatar Jason Gross2016-10-30
* Add InterpWfGravatar Jason Gross2016-10-28
* Add InterpWfRelGravatar Jason Gross2016-10-28
* Add beginnings of various interpretations of expression treesGravatar Jason Gross2016-10-27
* Merge pull request #84 from mit-plv/rsloan-phoasGravatar Jason Gross2016-10-27
|\
* | Add syntax and reification for the ops in GF25519Gravatar Jason Gross2016-10-27
* | Factor out cmov{l,ne} and negGravatar Jason Gross2016-10-27
* | Add WfRelReflectiveGravatar Jason Gross2016-10-27
* | Add WfReflectiveGenGravatar Jason Gross2016-10-27
* | Add Wf proofs about MapInterpGravatar Jason Gross2016-10-27
| * Merge branch 'master' into rsloan-phoasGravatar Jason Gross2016-10-27
| |\ | |/ |/|
* | Switch to bounded ZGravatar Jason Gross2016-10-25
| * Fix 8.4 buildGravatar Jason Gross2016-10-22
| * Merge branch 'master' into pr/84Gravatar Jason Gross2016-10-22
| |\ | |/ |/|
* | Fix src/Experiments/Ed25519.v for Coq 8.4Gravatar Jason Gross2016-10-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 07:10:00 +0000