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`.
---
 plugins/omega/PreOmega.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 1e0922e1ca..08bfec84bc 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -455,4 +455,4 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
 
 (** The complete Z-ification tactic *)
 
-Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem.
+Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op.
-- 
cgit v1.2.3