From 49eefc7b82f4939e9cedf5363af2a889c666fdcb Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Feb 2017 11:26:50 -0500 Subject: Add invert_Some; add nat_N_Z to push_Zof_N --- src/Util/ZUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/ZUtil.v') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 581ced889..04638a0c8 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -132,7 +132,7 @@ Hint Rewrite Nat2Z.id N2Z.id : zsimplify. Hint Rewrite Nat2Z.id : push_Zof_nat. Hint Rewrite N2Z.id : push_Zto_N. Hint Rewrite N2Z.id : pull_Zof_N. -Hint Rewrite N2Z.inj_pos N2Z.inj_abs_N N2Z.inj_add N2Z.inj_mul N2Z.inj_sub_max N2Z.inj_succ N2Z.inj_pred_max N2Z.inj_min N2Z.inj_max N2Z.inj_div N2Z.inj_quot N2Z.inj_rem N2Z.inj_div2 N2Z.inj_pow N2Z.inj_0 : push_Zof_N. +Hint Rewrite N2Z.inj_pos N2Z.inj_abs_N N2Z.inj_add N2Z.inj_mul N2Z.inj_sub_max N2Z.inj_succ N2Z.inj_pred_max N2Z.inj_min N2Z.inj_max N2Z.inj_div N2Z.inj_quot N2Z.inj_rem N2Z.inj_div2 N2Z.inj_pow N2Z.inj_0 nat_N_Z : push_Zof_N. Hint Rewrite N2Z.inj_compare N2Z.inj_testbit : pull_Zof_N. Hint Rewrite <- N2Z.inj_abs_N N2Z.inj_add N2Z.inj_mul N2Z.inj_sub_max N2Z.inj_succ N2Z.inj_pred_max N2Z.inj_min N2Z.inj_max N2Z.inj_div N2Z.inj_quot N2Z.inj_rem N2Z.inj_div2 N2Z.inj_pow : pull_Zof_N. Hint Rewrite Nat2Z.inj_0 Nat2Z.inj_succ Nat2Z.inj_abs_nat Nat2Z.inj_add Nat2Z.inj_mul Nat2Z.inj_sub_max Nat2Z.inj_pred_max Nat2Z.inj_min Nat2Z.inj_max Zabs2Nat.id_abs Zabs2Nat.id : push_Zof_nat. -- cgit v1.2.3