aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* Update _CoqProjectGravatar Jason Gross2017-01-21
* Add LetInMonad to _CoqProjectGravatar Jason Gross2017-01-19
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Split out Reflection.Equality, change Tflat implicit argumentGravatar Jason Gross2017-01-19
* More fine-grained util tactic filesGravatar Jason Gross2017-01-17
* Add curry.vGravatar Jason Gross2017-01-15
* Add ApplicationRelationsGravatar Jason Gross2017-01-10
* update-_CoqProjectGravatar Jason Gross2017-01-07
* Add reified LadderStep without carriesGravatar Jason Gross2017-01-07
* Revert "Add apply10"Gravatar Jason Gross2017-01-07
* copy_boundsGravatar Jason Gross2017-01-07
* Add fixed word size definitionsGravatar Jason Gross2017-01-03
* Add src/Reflection/MapCastWithCastOp.vGravatar Jason Gross2017-01-01
* Redo MultiSizeTest with generic frameworkGravatar Jason Gross2017-01-01
* Add generic code for MultiSizeTestGravatar Jason Gross2017-01-01
* make update-_CoqProjectGravatar Jason Gross2016-12-26
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 04:54:08 +0000