diff options
Diffstat (limited to 'plugins/micromega/ZCoeff.v')
| -rw-r--r-- | plugins/micromega/ZCoeff.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v index d65c60167..50197872c 100644 --- a/plugins/micromega/ZCoeff.v +++ b/plugins/micromega/ZCoeff.v @@ -93,6 +93,7 @@ Ltac le_less := rewrite (Rle_lt_eq sor); left; try assumption. Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption. Definition gen_order_phi_Z : Z -> R := gen_phiZ 0 1 rplus rtimes ropp. +Declare Equivalent Keys gen_order_phi_Z gen_phiZ. Notation phi_pos := (gen_phiPOS 1 rplus rtimes). Notation phi_pos1 := (gen_phiPOS1 1 rplus rtimes). |