aboutsummaryrefslogtreecommitdiff
path: root/contrib/romega/ROmega.v
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/romega/ROmega.v')
-rw-r--r--contrib/romega/ROmega.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v
index ba02b232e0..f1ffcf13d2 100644
--- a/contrib/romega/ROmega.v
+++ b/contrib/romega/ROmega.v
@@ -6,5 +6,5 @@
*************************************************************************)
-Require Omega.
-Require ReflOmegaCore.
+Require Import Omega.
+Require Import ReflOmegaCore. \ No newline at end of file