Move imports out of modules.

tuura · May 17, 2019 · 3711ed2 · 3711ed2
1 parent c9d809b
commit 3711ed2
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 8 deletions.
diff --git a/src/Control/Applicative.v b/src/Control/Applicative.v
@@ -1,6 +1,7 @@
 Require Export Hask.Ltac.
 Require Export Hask.Data.Functor.
 Require Export Hask.Data.Functor.Const.
+Require Import FunctionalExtensionality.
 
 Generalizable All Variables.
 
@@ -44,8 +45,6 @@ Module ApplicativeLaws.
 
 Include FunctorLaws.
 
-Require Import FunctionalExtensionality.
-
 Class ApplicativeLaws (f : Type -> Type) `{Applicative f} := {
   has_functor_laws :> FunctorLaws f;
 

diff --git a/src/Data/Functor.v b/src/Data/Functor.v
@@ -1,4 +1,7 @@
 Require Import Hask.Ltac.
+Require Import FunctionalExtensionality.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Setoids.Setoid.
 
 Generalizable All Variables.
 
@@ -23,10 +26,6 @@ Notation "fmap[ M N O ]" :=
 
 Module FunctorLaws.
 
-Require Import FunctionalExtensionality.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
-
 (* Functors preserve extensional equality for the applied function.
    This is needed to perform setoid rewriting within the function
    passed to a functor. *)

diff --git a/src/Data/Functor/Contravariant.v b/src/Data/Functor/Contravariant.v
@@ -1,5 +1,6 @@
 Require Import Hask.Ltac.
 Require Import Hask.Data.Functor.
+Require Import FunctionalExtensionality.
 
 Generalizable All Variables.
 
@@ -31,8 +32,6 @@ Module ContravariantLaws.
 
 Include FunctorLaws.
 
-Require Import FunctionalExtensionality.
-
 Class ContravariantLaws (f : Type -> Type) `{Contravariant f} := {
   contramap_id   : forall a : Type, contramap (@id a) = id;
   contramap_comp : forall (a b c : Type) (f : b -> c) (g : a -> b),