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.v12
1 files changed, 0 insertions, 12 deletions
diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v
deleted file mode 100644
index 4281cc57..00000000
--- a/contrib/romega/ROmega.v
+++ /dev/null
@@ -1,12 +0,0 @@
-(*************************************************************************
-
- PROJET RNRT Calife - 2001
- Author: Pierre Crégut - France Télécom R&D
- Licence : LGPL version 2.1
-
- *************************************************************************)
-
-Require Import ReflOmegaCore.
-Require Export Setoid.
-Require Export PreOmega.
-Require Export ZArith_base.