From a10076e834720c05e55397c9e26b9d7a8786298b Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 3 Dec 2018 18:10:03 -0500
Subject: Move cleanup from the test-suite to Z.div_mod_to_quot_rem_cleanup

Also fold it into `Z.div_mod_to_quot_rem`

Note that the test-suite file is a bit slow.  On my machine, it is

```
real    2m32.983s
user    2m32.544s
sys     0m0.492s
```
---
 plugins/omega/PreOmega.v | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 08bfec84bc..7ebc2fb04f 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -16,7 +16,8 @@ Local Open Scope Z_scope.
 
 (** This tactic uses the complete specification of [Z.div] and
     [Z.modulo] to remove these functions from the goal without losing
-    information. *)
+    information.  The [Z.div_mod_to_quot_rem_cleanup] tactic removes
+    needless hypotheses, which makes tactics like [nia] run faster. *)
 
 Module Z.
   Lemma mod_0_r_ext x y : y = 0 -> x mod y = 0.
@@ -42,7 +43,16 @@ Module Z.
     | [ H : context[?x / ?y] |- _ ] => div_mod_to_quot_rem_generalize x y
     | [ H : context[?x mod ?y] |- _ ] => div_mod_to_quot_rem_generalize x y
     end.
-  Ltac div_mod_to_quot_rem := repeat div_mod_to_quot_rem_step.
+  Ltac div_mod_to_quot_rem' := repeat div_mod_to_quot_rem_step.
+  Ltac div_mod_to_quot_rem_cleanup :=
+    repeat match goal with
+           | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H')
+           | [ H : ?T -> _, H' : ~?T |- _ ] => clear H
+           | [ H : ~?T -> _, H' : ?T |- _ ] => clear H
+           | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
+           | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
+           end.
+  Ltac div_mod_to_quot_rem := div_mod_to_quot_rem'; div_mod_to_quot_rem_cleanup.
 End Z.
 
 (** * zify: the Z-ification tactic *)
-- 
cgit v1.2.3