aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xcontrib/omega/Omega.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index 13a7642539..8c646ae087 100755
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
@@ -12,7 +12,6 @@ Require Export ZArith.
(* The constant minus is required in coq_omega.ml *)
Require Export Minus.
-Declare ML Module "equality".
Declare ML Module "omega".
Declare ML Module "coq_omega".