diff options
Diffstat (limited to 'plugins/omega/Omega.v')
| -rw-r--r-- | plugins/omega/Omega.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v index 3f9d0f448..6cdfea43f 100644 --- a/plugins/omega/Omega.v +++ b/plugins/omega/Omega.v @@ -19,9 +19,9 @@ Require Export OmegaLemmas. Require Export PreOmega. Declare ML Module "omega_plugin". -Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l - Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l - Zmult_plus_distr_r: zarith. +Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l + Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_r + Z.mul_add_distr_l: zarith. Require Export Zhints. |