aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--CHANGES6
-rw-r--r--plugins/omega/Omega.v8
-rw-r--r--plugins/omega/OmegaPlugin.v6
-rw-r--r--plugins/omega/OmegaTactic.v15
-rw-r--r--plugins/omega/vo.itarget1
-rw-r--r--theories/Reals/Cos_rel.v2
6 files changed, 28 insertions, 10 deletions
diff --git a/CHANGES b/CHANGES
index 982b96a11..13433c49b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -258,9 +258,9 @@ Tactics
- Behavior of introduction patterns -> and <- made more uniform
(hypothesis is cleared, rewrite in hypotheses and conclusion and
erasing the variable when rewriting a variable).
-- Tactics from plugins are now active only when the corresponding
- module is imported (source of incompatibilities, solvable by adding
- an "Import", like e.g. "Import Omega").
+- Tactics from plugins are now active only when the corresponding module
+ is imported (source of incompatibilities, solvable by adding an "Import";
+ in the particular case of Omega, use "Require Import OmegaTactic").
- Semantics of destruct/induction has been made more regular in some
edge cases, possibly leading to incompatibilities:
- new goals are now opened when the term does not match a subterm of
diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v
index 7400d4629..a5f90dd66 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 9e5c14841..9f101dbf2 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 000000000..9f101dbf2
--- /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 9d9a77a8c..842210e21 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
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index cfb30662b..6d30319c9 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -10,7 +10,7 @@ Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Rtrigo_def.
-Require Import Omega.
+Require Import OmegaTactic.
Local Open Scope R_scope.
Definition A1 (x:R) (N:nat) : R :=