diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-15 00:09:39 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-15 00:12:44 -0400 |
| commit | 557e24e4a2a097e69eba61696758aa3ee25ebbb7 (patch) | |
| tree | 45233771b678c7653a05e48b206a3e8576a2fb4a /src/Util/ZRange.v | |
| parent | fe63118de92560724d27c5e3f3ad84a5b210cdfc (diff) | |
More powerful inversion_zrange
Diffstat (limited to 'src/Util/ZRange.v')
| -rw-r--r-- | src/Util/ZRange.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/ZRange.v b/src/Util/ZRange.v index 2c286aa9e..489d2c32f 100644 --- a/src/Util/ZRange.v +++ b/src/Util/ZRange.v @@ -17,6 +17,12 @@ Ltac inversion_zrange := | [ H : _ = _ :> zrange |- _ ] => pose proof (f_equal lower H); pose proof (f_equal upper H); clear H; cbv beta iota in * + | [ H : Build_zrange _ _ = _ |- _ ] + => pose proof (f_equal lower H); pose proof (f_equal upper H); clear H; + cbv beta iota in * + | [ H : _ = Build_zrange _ _ |- _ ] + => pose proof (f_equal lower H); pose proof (f_equal upper H); clear H; + cbv beta iota in * end. (** All of the boundedness properties take an optional bitwidth, and |