diff options
Diffstat (limited to 'theories/micromega/Zify.v')
| -rw-r--r-- | theories/micromega/Zify.v | 15 |
1 files changed, 13 insertions, 2 deletions
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. |