From 2e3d67952aff6115983a012b3c8420fa9297a1dd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 21 Mar 2017 17:28:27 -0400 Subject: Split off the extra power of rewrite_mod_small into rewrite_mod_mod_small --- src/Util/ZUtil.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Util/ZUtil.v') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 64604022a..2d3f24c07 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -2566,6 +2566,13 @@ Module Z. | [ |- context[(?a mod ?n) mod ?m] ] => rewrite (mod_mod_small a n m) by rewrite_mod_small_solver end. + Ltac rewrite_mod_mod_small := + repeat match goal with + | [ |- context[(?a mod ?n) mod ?m] ] + => rewrite (mod_mod_small a n m) by rewrite_mod_small_solver + end. + Ltac rewrite_mod_small_more := + repeat (rewrite_mod_small || rewrite_mod_mod_small). Local Ltac simplify_div_tac := intros; autorewrite with zsimplify; rewrite <- ?Z_div_plus_full_l, <- ?Z_div_plus_full by assumption; -- cgit v1.2.3