diff options
Diffstat (limited to 'contrib/omega/Omega.v')
| -rwxr-xr-x | contrib/omega/Omega.v | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v index 6c4a6191b..7da167623 100755 --- a/contrib/omega/Omega.v +++ b/contrib/omega/Omega.v @@ -19,11 +19,6 @@ Require Export ZArith. (* The constant minus is required in coq_omega.ml *) Require Export Minus. -Declare ML Module "omega". -Declare ML Module "coq_omega". - -Require Export OmegaSyntax. - Hint eq_nat_Omega : zarith := Extern 10 (eq nat ? ?) Abstract Omega. Hint le_Omega : zarith := Extern 10 (le ? ?) Abstract Omega. Hint lt_Omega : zarith := Extern 10 (lt ? ?) Abstract Omega. |