summaryrefslogtreecommitdiff
path: root/contrib/romega/ROmega.v
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/romega/ROmega.v')
-rw-r--r--contrib/romega/ROmega.v5
1 files changed, 3 insertions, 2 deletions
diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v
index 19933873..68bc43bb 100644
--- a/contrib/romega/ROmega.v
+++ b/contrib/romega/ROmega.v
@@ -1,10 +1,11 @@
(*************************************************************************
PROJET RNRT Calife - 2001
- Author: Pierre Crégut - France Télécom R&D
+ Author: Pierre Crégut - France Télécom R&D
Licence : LGPL version 2.1
*************************************************************************)
Require Import ReflOmegaCore.
-
+Require Export Setoid.
+Require Export PreOmega.