aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/Zify.v
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-01-14 22:45:13 +0100
committerPierre-Marie Pédrot2020-01-14 22:45:13 +0100
commita7e788403cae2c82bcb2b39f8576318a175ee788 (patch)
treecfa7f6b37676c10ad525fad4d89be81d9d6ae1c2 /plugins/micromega/Zify.v
parent46bcb69007811b957087b82a8b74c3c411229081 (diff)
parent4f0703eaabbe80d3624721982a7ab50254616b4a (diff)
Merge PR #11370: [zify] elim let in ML
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/micromega/Zify.v')
-rw-r--r--plugins/micromega/Zify.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/Zify.v b/plugins/micromega/Zify.v
index 785a53fafa..18cd196148 100644
--- a/plugins/micromega/Zify.v
+++ b/plugins/micromega/Zify.v
@@ -87,4 +87,4 @@ Ltac applySpec S :=
(** [zify_post_hook] is there to be redefined. *)
Ltac zify_post_hook := idtac.
-Ltac zify := zify_op ; (iter_specs applySpec) ; zify_post_hook.
+Ltac zify := zify_op ; (zify_iter_specs applySpec) ; zify_post_hook.