From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Wed, 15 Jul 2015 10:36:12 +0200
Subject: Imported Upstream version 8.5~beta2+dfsg

---
 plugins/omega/Omega.v       |  8 ++------
 plugins/omega/OmegaPlugin.v |  6 ++++++
 plugins/omega/OmegaTactic.v | 15 +++++++++++++++
 plugins/omega/vo.itarget    |  1 +
 4 files changed, 24 insertions(+), 6 deletions(-)
 create mode 100644 plugins/omega/OmegaTactic.v

(limited to 'plugins/omega')

diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v
index 7400d462..a5f90dd6 100644
--- a/plugins/omega/Omega.v
+++ b/plugins/omega/Omega.v
@@ -13,10 +13,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* We do not require [ZArith] anymore, but only what's necessary for Omega *)
+(* We import what is necessary for Omega *)
 Require Export ZArith_base.
 Require Export OmegaLemmas.
 Require Export PreOmega.
+
 Declare ML Module "omega_plugin".
 
 Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l
@@ -25,11 +26,6 @@ Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l
 
 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.
diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v
index 9e5c1484..9f101dbf 100644
--- a/plugins/omega/OmegaPlugin.v
+++ b/plugins/omega/OmegaPlugin.v
@@ -6,4 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* To strictly import the omega tactic *)
+
+Require ZArith_base.
+Require OmegaLemmas.
+Require PreOmega.
+
 Declare ML Module "omega_plugin".
diff --git a/plugins/omega/OmegaTactic.v b/plugins/omega/OmegaTactic.v
new file mode 100644
index 00000000..9f101dbf
--- /dev/null
+++ b/plugins/omega/OmegaTactic.v
@@ -0,0 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* To strictly import the omega tactic *)
+
+Require ZArith_base.
+Require OmegaLemmas.
+Require PreOmega.
+
+Declare ML Module "omega_plugin".
diff --git a/plugins/omega/vo.itarget b/plugins/omega/vo.itarget
index 9d9a77a8..842210e2 100644
--- a/plugins/omega/vo.itarget
+++ b/plugins/omega/vo.itarget
@@ -1,4 +1,5 @@
 OmegaLemmas.vo
 OmegaPlugin.vo
+OmegaTactic.vo
 Omega.vo
 PreOmega.vo
-- 
cgit v1.2.3