From 66c523bcac8b64e202baa084bf24f5b57c61fcd6 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 6 Mar 2018 16:12:28 +0000
Subject: [stdlib] Do not use “Require” inside sections

---
 plugins/micromega/RingMicromega.v | 3 ++-
 plugins/nsatz/Nsatz.v             | 6 +++---
 plugins/rtauto/Rtauto.v           | 4 +---
 3 files changed, 6 insertions(+), 7 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 543a37ff8d..f066ea462f 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 85e2a5b235..c5a09d677e 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 db17c0d654..19b3ab397d 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 :
-- 
cgit v1.2.3