From 031af730ae12601127d71b18adfc54d1a94eaaac Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Tue, 7 Jul 2020 10:14:44 +0200 Subject: [zify] Use flag for Z.to_euclidean_division_equations. Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross Co-authored-by: Jim Fehrle --- theories/micromega/Zify.v | 15 +++++++++++++-- theories/micromega/ZifyInt63.v | 3 +-- 2 files changed, 14 insertions(+), 4 deletions(-) (limited to 'theories/micromega') 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). -- cgit v1.2.3