From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 contrib/omega/Omega.v | 58 ---------------------------------------------------
 1 file changed, 58 deletions(-)
 delete mode 100644 contrib/omega/Omega.v

(limited to 'contrib/omega/Omega.v')

diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
deleted file mode 100644
index ee823502..00000000
--- a/contrib/omega/Omega.v
+++ /dev/null
@@ -1,58 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-(**************************************************************************)
-(*                                                                        *)
-(* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
-(*                                                                        *)
-(* Pierre Crégut (CNET, Lannion, France)                                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* $Id: Omega.v 10028 2007-07-18 22:38:06Z letouzey $ *)
-
-(* We do not require [ZArith] anymore, but only what's necessary for Omega *)
-Require Export ZArith_base.
-Require Export OmegaLemmas.
-Require Export PreOmega.
-
-Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
-  Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
-  Zmult_plus_distr_r: zarith.
-
-Require Export Zhints.
-
-(*
-(* The constant minus is required in coq_omega.ml *)
-Require Minus.
-*)
-
-Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith.
-Hint Extern 10 (_ <= _) => abstract omega: zarith.
-Hint Extern 10 (_ < _) => abstract omega: zarith.
-Hint Extern 10 (_ >= _) => abstract omega: zarith.
-Hint Extern 10 (_ > _) => abstract omega: zarith.
-
-Hint Extern 10 (_ <> _ :>nat) => abstract omega: zarith.
-Hint Extern 10 (~ _ <= _) => abstract omega: zarith.
-Hint Extern 10 (~ _ < _) => abstract omega: zarith.
-Hint Extern 10 (~ _ >= _) => abstract omega: zarith.
-Hint Extern 10 (~ _ > _) => abstract omega: zarith.
-
-Hint Extern 10 (_ = _ :>Z) => abstract omega: zarith.
-Hint Extern 10 (_ <= _)%Z => abstract omega: zarith.
-Hint Extern 10 (_ < _)%Z => abstract omega: zarith.
-Hint Extern 10 (_ >= _)%Z => abstract omega: zarith.
-Hint Extern 10 (_ > _)%Z => abstract omega: zarith.
-
-Hint Extern 10 (_ <> _ :>Z) => abstract omega: zarith.
-Hint Extern 10 (~ (_ <= _)%Z) => abstract omega: zarith.
-Hint Extern 10 (~ (_ < _)%Z) => abstract omega: zarith.
-Hint Extern 10 (~ (_ >= _)%Z) => abstract omega: zarith.
-Hint Extern 10 (~ (_ > _)%Z) => abstract omega: zarith.
-
-Hint Extern 10 False => abstract omega: zarith.
\ No newline at end of file
-- 
cgit v1.2.3