aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-08 10:11:49 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-08 10:11:49 +0100
commitc31c6d92d2b2c314ea9c633f9e0f14500c2785b0 (patch)
tree7cd0f3c56b5b1e6dbf433e66e1d03fbb89d1f8a8 /plugins
parentc5cd6f93bc14c66a3e4d7e17f8d18dc9fb2308d7 (diff)
parent5cbb460234e32f5e325c60aaada91d3cea298b9f (diff)
Merge PR #6934: Warn when using “Require” in a section
Diffstat (limited to 'plugins')
-rw-r--r--plugins/micromega/RingMicromega.v3
-rw-r--r--plugins/nsatz/Nsatz.v6
-rw-r--r--plugins/rtauto/Rtauto.v4
3 files changed, 6 insertions, 7 deletions
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 543a37ff8..f066ea462 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -21,6 +21,7 @@ Require Import List.
Require Import Bool.
Require Import OrderedRing.
Require Import Refl.
+Require Coq.micromega.Tauto.
Set Implicit Arguments.
@@ -796,7 +797,7 @@ Definition xnormalise (t:Formula C) : list (NFormula) :=
| OpLe => (psub lhs rhs ,Strict) :: nil
end.
-Require Import Coq.micromega.Tauto.
+Import Coq.micromega.Tauto.
Definition cnf_normalise (t:Formula C) : cnf (NFormula) :=
List.map (fun x => x::nil) (xnormalise t).
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index 85e2a5b23..c5a09d677 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -30,6 +30,7 @@ Require Export Ncring_initial.
Require Export Ncring_tac.
Require Export Integral_domain.
Require Import DiscrR.
+Require Import ZArith.
Declare ML Module "nsatz_plugin".
@@ -56,9 +57,8 @@ simpl. simpl; cring.
Qed.
(* adpatation du code de Benjamin aux setoides *)
-Require Import ZArith.
-Require Export Ring_polynom.
-Require Export InitialRing.
+Export Ring_polynom.
+Export InitialRing.
Definition PolZ := Pol Z.
Definition PEZ := PExpr Z.
diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v
index db17c0d65..19b3ab397 100644
--- a/plugins/rtauto/Rtauto.v
+++ b/plugins/rtauto/Rtauto.v
@@ -11,7 +11,7 @@
Require Export List.
Require Export Bintree.
-Require Import Bool.
+Require Import Bool BinPos.
Declare ML Module "rtauto_plugin".
@@ -98,8 +98,6 @@ match F with
| F_push H hyps0 F0 => interp_ctx hyps0 F0 ([[H]] -> G)
end.
-Require Export BinPos.
-
Ltac wipe := intros;simpl;constructor.
Lemma compose0 :