diff options
Diffstat (limited to 'contrib/omega/Omega.v')
| -rw-r--r-- | contrib/omega/Omega.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v index 3b427162e..30b945718 100644 --- a/contrib/omega/Omega.v +++ b/contrib/omega/Omega.v @@ -19,6 +19,7 @@ Require Export ZArith_base. 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 |