aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly/Evaluables.v
Commit message (Expand)AuthorAge
* Refactors to remove intermediate conversionsGravatar Robert Sloan2016-10-26
* Refactors to remove intermediate conversions in HLConversionsGravatar Robert Sloan2016-10-25
* Merge branch 'rsloan-phoas' of github.com:mit-plv/fiat-crypto into rsloan-phoasGravatar Robert Sloan2016-10-24
|\
* | Use HL conversions for all data types + Pipeline.v refactorsGravatar Robert Sloan2016-10-24
| * Fix 8.4 buildGravatar Jason Gross2016-10-22
|/
* Make lower bounds work by using HL conversionsGravatar Robert Sloan2016-10-21
* merge rsloan-phoas refactors into masterGravatar Robert Sloan2016-10-21
|\
* | committing unstable refactors to patch masterGravatar Robert Sloan2016-10-21
| * Various fixes for Coq 8.4Gravatar Jason Gross2016-10-20
|/
* Fast bounds-checking machinery but lower-bounds are brokenGravatar Robert Sloan2016-10-18
* Converting to bounded machineryGravatar Robert Sloan2016-10-17
* More of the Conversions.v correctness proofsGravatar Robert Sloan2016-10-14
* Making sub bounds actually tightGravatar Robert Sloan2016-10-14
* More minor improvements in Conversions.v and Compile.vGravatar Robert Sloan2016-10-13
* Large-scale refactoring of src/AssemblyGravatar Robert Sloan2016-09-24
* Finished more efficient WordRangeOptGravatar Robert Sloan2016-09-15
* Most of a more efficient WordRangeOptGravatar Robert Sloan2016-09-13
* Fix evalWordRangeOptGravatar Robert Sloan2016-08-26
* Much tighter bounds in Evaluables.vGravatar Robert Sloan2016-08-26
* Removed nat arguments to Evaluable operationsGravatar Robert Sloan2016-08-25
* Finishing tactical machinery for bound-computingGravatar Robert Sloan2016-08-24
* Experimental requirements for rsloan-phoasGravatar Robert Sloan2016-08-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 01:36:16 +0000