aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/omega/PreOmega.v2
1 files changed, 1 insertions, 1 deletions
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.