From 0c99020482e96ceb05799c47ffbcaef0e89b4b1f Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 3 Dec 2018 16:45:49 -0500
Subject: Don't bundle Z.div_mod_quot_rem into zify

Alas, I have not had time to work on imrpoving the performance of nia,
and there has been a request to include this tactic (which is useful on
its own) without bundling it into `zify`.  So that is what we do here.

I leave the definition of it in `PreOmega` in case we want to eventually
include it in `zify`/`nia`.
---
 test-suite/success/Nia.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index da0b2a7a83..9a13e41e07 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -2,6 +2,9 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia.
 Open Scope Z_scope.
 
+(** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this 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