diff options
| author | Frédéric Besson | 2020-07-07 10:14:44 +0200 |
|---|---|---|
| committer | BESSON Frederic | 2020-10-20 10:02:19 +0200 |
| commit | 031af730ae12601127d71b18adfc54d1a94eaaac (patch) | |
| tree | 97443f67a20600c6e5688fd2a1a36ca4d05b25ca /theories/micromega | |
| parent | a2f5cc26baca0db087a677196f186ac2f75aa484 (diff) | |
[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>
Diffstat (limited to 'theories/micromega')
| -rw-r--r-- | theories/micromega/Zify.v | 15 | ||||
| -rw-r--r-- | theories/micromega/ZifyInt63.v | 3 |
2 files changed, 14 insertions, 4 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. 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). |