aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega/Omega.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/omega/Omega.v')
-rw-r--r--plugins/omega/Omega.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v
index 30b945718..6d0b6bae1 100644
--- a/plugins/omega/Omega.v
+++ b/plugins/omega/Omega.v
@@ -13,8 +13,6 @@
(* *)
(**************************************************************************)
-(* $Id$ *)
-
(* We do not require [ZArith] anymore, but only what's necessary for Omega *)
Require Export ZArith_base.
Require Export OmegaLemmas.