From 557e24e4a2a097e69eba61696758aa3ee25ebbb7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 15 Apr 2017 00:09:39 -0400 Subject: More powerful inversion_zrange --- src/Util/ZRange.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/Util/ZRange.v') 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 -- cgit v1.2.3