Fun functors visibility (#90)

Close #88
coq-community · Jun 3, 2020 · f8f530a · f8f530a
1 parent 973e4bb
commit f8f530a
Showing 1 changed file with 2 additions and 6 deletions.
diff --git a/theories/Data/Fun.v b/theories/Data/Fun.v
@@ -11,11 +11,7 @@ Set Strict Implicit.
 Section functors.
   Variable A : Type.
 
-  Instance FunFunctor A : Functor (Fun A) :=
-  { fmap _A _B g f x := g (f x)
-  }.
-
-  Local Instance Functor_Fun : Functor (Fun A) :=
+  Global Instance Functor_Fun : Functor (Fun A) :=
   { fmap _A _B g f x := g (f x) }.
 
   Local Instance CoFunctor_Fun T : CoFunctor (fun x => x -> T) :=
@@ -33,7 +29,7 @@ Section functors.
   Local Instance CoFunctor_cofunctor F G (fF : CoFunctor F) (fG : CoFunctor G) : Functor (fun x => F (G x)) :=
   {| fmap := fun _ _ g => @cofmap F _ _ _ (@cofmap G _ _ _ g) |}.
 
-  Local Instance Applicative_Fun : Applicative (Fun A) :=
+  Global Instance Applicative_Fun : Applicative (Fun A) :=
   { pure := fun _ x _ => x
   ; ap := fun _ _ f x y => (f y) (x y)
   }.