From 6e5dfa6ad6aca6aa19b7d1348817bd2c23d8fdad Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 13 May 2017 11:55:41 -0400 Subject: Split off more of ZUtil --- src/Util/ZUtil/Tactics/CompareToSgn.v | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 src/Util/ZUtil/Tactics/CompareToSgn.v (limited to 'src/Util/ZUtil/Tactics/CompareToSgn.v') diff --git a/src/Util/ZUtil/Tactics/CompareToSgn.v b/src/Util/ZUtil/Tactics/CompareToSgn.v new file mode 100644 index 000000000..31588815b --- /dev/null +++ b/src/Util/ZUtil/Tactics/CompareToSgn.v @@ -0,0 +1,8 @@ +Require Import Coq.ZArith.ZArith. +Module Z. + Ltac compare_to_sgn := + repeat match goal with + | [ H : _ |- _ ] => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff in H + | _ => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff + end. +End Z. -- cgit v1.2.3