Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Remove BoundedWord | Benjamin Barenblat | 2019-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 BoundedWord | Jason Gross | 2017-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.v | Jason Gross | 2017-04-01 |