fix deprecated warnings.

Author: gmalecha

theories/Data/Map/FMapAList.v

@@ -1,4 +1,5 @@
-Require Import List.
+Require Import Coq.Classes.RelationClasses.
+Require Import Coq.Lists.List.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Structures.Maps.
@@ -63,7 +64,6 @@ Section keyed.
 
   Section proofs.
     Hypothesis RDC_K : RelDec_Correct RD_K.
-    Require Import RelationClasses.
 
     Hypothesis Refl : Reflexive R.
     Hypothesis Sym : Symmetric R.

theories/Data/Map/FMapPositive.v

@@ -239,8 +239,9 @@ Section fmap.
 
 End fmap.
 
+Require Import ExtLib.Core.Type.
+
 Section type.
-  Require Import ExtLib.Core.Type.
   Variable T : Type.
   Variable tT : type T.
 

theories/Data/Map/FMapTwoThreeK.v

@@ -1,7 +1,8 @@
-Require Import ExtLib.Structures.Maps.
-Require Import List.
+Require Import Coq.Lists.List.
 Require Import ExtLib.Core.RelDec.
+Require Import ExtLib.Structures.Maps.
 Require Import ExtLib.Structures.Monads.
+Require Import ExtLib.Structures.Reducible.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -150,8 +151,6 @@ Section keyed.
   ; union  := twothree_union
   }.
 
-  Require Import ExtLib.Structures.Reducible.
-
   Global Instance Foldable_twothree V : Foldable (twothree V) (K * V) :=
     fun _ f b x => twothree_fold (fun k v => f (k,v)) b x.