[stdlib] Do not use “Require” inside sections

4 files changed, 5 insertions, 9 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 9fd52866e..238ac7df0 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -28,6 +28,8 @@ intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005.
 [[Werner97]] Benjamin Werner, Sets in Types, Types in Sets, TACS, 1997.
 *)
 
+Require Import RelationClasses Logic.
+
 Set Implicit Arguments.
 Local Unset Intuition Negation Unfolding.
 
@@ -125,8 +127,6 @@ Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) :=
    formulation of choice); Note also a typo in its intended
    formulation in [[Werner97]]. *)
 
-Require Import RelationClasses Logic.
-
 Definition RepresentativeFunctionalChoice_on :=
   forall R:A->A->Prop,
     (Equivalence R) ->
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index a50140628..a79ddead2 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -11,6 +11,7 @@
 (* G. Huet 1-9-95 *)
 
 Require Import Permut Setoid.
+Require Plus. (* comm. and ass. of plus *)
 
 Set Implicit Arguments.
 
@@ -69,9 +70,6 @@ Section multiset_defs.
     unfold meq; unfold munion; simpl; auto.
   Qed.
 
-
-  Require Plus. (* comm. and ass. of plus *)
-
   Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
   Proof.
     unfold meq; unfold multiplicity; unfold munion.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 95ba93232..7940bda1a 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -13,7 +13,7 @@
 (* G. Huet 1-9-95 *)
 (* Updated Papageno 12/98 *)
 
-Require Import Bool.
+Require Import Bool Permut.
 
 Set Implicit Arguments.
 
@@ -140,8 +140,6 @@ Hint Resolve seq_right.
 (** Here we should make uniset an abstract datatype, by hiding [Charac],
     [union], [charac]; all further properties are proved abstractly *)
 
-Require Import Permut.
-
 Lemma union_rotate :
  forall x y z:uniset, seq (union x (union y z)) (union z (union x y)).
 Proof.
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 8f583be97..d9e5ad676 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -136,7 +136,7 @@ Section defs.
       (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
       (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) ->
       merge_lem l1 l2.
-  Require Import Morphisms.
+  Import Morphisms.
   
   Instance: Equivalence (@meq A).
   Proof. constructor; auto with datatypes. red. apply meq_trans. Defined.