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 ++++++++++++--
 test-suite/success/Nia.v | 15 ++-------------
 2 files changed, 14 insertions(+), 15 deletions(-)

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 *)
diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index b79a6bde3d..6cb645d9eb 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -2,20 +2,9 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia.
 Open Scope Z_scope.
 
-Ltac 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
-         | _ => progress subst
-         end.
-
 (** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this
-    file.  Note that we also add a [cleanup] tactic, which is very
-    important for speed purposes. *)
-Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem; cleanup.
+    file. *)
+Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem.
 
 Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed.
 Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed.
-- 
cgit v1.2.3