diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-21 16:27:24 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-21 16:27:24 -0400 |
| commit | ec980c530589f89fd008cc0c015a985aaed9fd1e (patch) | |
| tree | 245825204c4f9093d879be79a6ace24bd48708c8 /src/Util/Bool.v | |
| parent | d4690fb9073f3d9d037acdf2b3655397af406974 (diff) | |
Make Z.ltb_to_lt a bit stronger
Now it works not just at top-level, but also in, e.g., arguments to
hypotheses.
We had to change some proofs because it no longer moves the hypotheses
it changes to the bottom.
Diffstat (limited to 'src/Util/Bool.v')
0 files changed, 0 insertions, 0 deletions