aboutsummaryrefslogtreecommitdiff
path: root/src/Util/BoundedWord.v
Commit message (Collapse)AuthorAge
* Remove BoundedWordGravatar Benjamin Barenblat2019-04-26
| | | | | | Remove Util/BoundedWord.v and its reverse dependencies Util/FixedWordSizes.v and Util/FixedWordSizesEquality.v. This code is no longer in use.
* Fix definition of BoundedWordGravatar Jason Gross2017-04-01
| | | | | | | We need to take log2, because wordT takes lg(wordsize). We need to pass None rather than Some, because None means "the original output type of the function we're reifying is a tuple of Z" (as opposed to a tuple of words), which is the situation we're in.
* Split off BoundedWord.v from IntegrationTest.vGravatar Jason Gross2017-04-01