[zify] Use flag for Z.to_euclidean_division_equations.

Update doc/sphinx/addendum/micromega.rst

Co-authored-by: Jason Gross <jasongross9@gmail.com>
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

4 files changed, 19 insertions, 7 deletions

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 01aed122b2..b3a33ffeea 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -283,8 +283,8 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 .. tacn:: zify
    :name: zify
 
-   This tactic is internally called by :tacn:`lia` to support additional types e.g., :g:`nat`, :g:`positive` and :g:`N`.
-   Some additional support is provided by the following modules
+   This tactic is internally called by :tacn:`lia` to support additional types, e.g., :g:`nat`, :g:`positive` and :g:`N`.
+   Additional support is provided by the following modules:
 
    + For boolean operators (e.g., :g:`Nat.leb`), require the module :g:`ZifyBool`.
    + For comparison operators (e.g., :g:`Z.compare`), require the module :g:`ZifyComparison`.
@@ -295,7 +295,7 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 
    + To support :g:`Z.div` and :g:`Z.modulo`: ``Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations``.
    + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``.
-   + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations``.
+   + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot` and :g:`Z.rem`: either ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations`` or ``Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true)``.
 
    The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands.
    The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``.
diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v
index 183fd6a914..01cc9ad810 100644
--- a/theories/micromega/Zify.v
+++ b/theories/micromega/Zify.v
@@ -16,11 +16,22 @@ Ltac zify_pre_hook := idtac.
 
 Ltac zify_post_hook := idtac.
 
-Ltac iter_specs := zify_iter_specs.
+Ltac zify_convert_to_euclidean_division_equations_flag := constr:(false).
+
+(** [zify_internal_to_euclidean_division_equations] is bound in [PreOmega] *)
+Ltac zify_internal_to_euclidean_division_equations := idtac.
+
+Ltac zify_to_euclidean_division_equations :=
+  lazymatch zify_convert_to_euclidean_division_equations_flag with
+  | true => zify_internal_to_euclidean_division_equations
+  | false => idtac
+  end.
+
 
 Ltac zify := intros;
              zify_pre_hook ;
              zify_elim_let ;
              zify_op ;
              (zify_iter_specs) ;
-             zify_saturate ; zify_post_hook.
+             zify_saturate ;
+             zify_to_euclidean_division_equations ; zify_post_hook.
diff --git a/theories/micromega/ZifyInt63.v b/theories/micromega/ZifyInt63.v
index 69f3502d8c..27845898aa 100644
--- a/theories/micromega/ZifyInt63.v
+++ b/theories/micromega/ZifyInt63.v
@@ -175,5 +175,4 @@ Instance Op_is_even : UnOp is_even :=
 Add Zify UnOp Op_is_even.
 
 
-
-Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
+Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true).
diff --git a/theories/omega/PreOmega.v b/theories/omega/PreOmega.v
index 506a4108ee..70f25e7243 100644
--- a/theories/omega/PreOmega.v
+++ b/theories/omega/PreOmega.v
@@ -573,4 +573,6 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
 Require  Import ZifyClasses ZifyInst.
 Require  Zify.
 
+Ltac Zify.zify_internal_to_euclidean_division_equations ::= Z.to_euclidean_division_equations.
+
 Ltac zify := Zify.zify.