aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/omega/PreOmega.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 60e606a687..aa48edcbcc 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -400,6 +400,5 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
(** The complete Z-ification tactic *)
-Ltac zify :=
- repeat progress (zify_nat; zify_positive; zify_N); zify_op.
+Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op.