From 8581e1a977518c354eb06820d3513238412af7de Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 30 Mar 2015 22:15:02 +0200
Subject: Accomodating #4166 (providing "Require Import OmegaTactic" as a
 replacement for 8.4's "Require Omega").

---
 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')

diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v
index 7400d4629d..a5f90dd66e 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 9e5c148411..9f101dbf2e 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 0000000000..9f101dbf2e
--- /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 9d9a77a8c2..842210e216 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