X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneralizedArrow.v;h=bf7743b6f6a1b2b800c3a001740adcc67a5fe7af;hp=f2465675526f995ae95338299713edf1888cf5c6;hb=992203bb4a221ea2f415c0d14bb34d35af2ee637;hpb=f60f9ed58ad2ea12fd293dfbcc015c3ffb827a20

diff --git a/src/GeneralizedArrow.v b/src/GeneralizedArrow.v
index f246567..bf7743b 100644
--- a/src/GeneralizedArrow.v
+++ b/src/GeneralizedArrow.v
@@ -22,14 +22,14 @@ Require Import Coherence_ch7_8.
 Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.
 
-Class GeneralizedArrow (K:Enrichment) (C:MonoidalEnrichment) :=
+Class GeneralizedArrow (K:Enrichment) {ce}(C:MonoidalEnrichment ce) :=
 { ga_functor_obj      : enr_v_mon K -> C
 ; ga_functor          : Functor (enr_v_mon K) C ga_functor_obj
 ; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) C ga_functor
 }.
 Coercion ga_functor_monoidal : GeneralizedArrow >-> MonoidalFunctor.
 
-Implicit Arguments GeneralizedArrow    [ ].
-Implicit Arguments ga_functor_obj      [ K C ].
-Implicit Arguments ga_functor          [ K C ].
-Implicit Arguments ga_functor_monoidal [ K C ].
+Implicit Arguments GeneralizedArrow    [ [ce] ].
+Implicit Arguments ga_functor_obj      [ K ce C ].
+Implicit Arguments ga_functor          [ K ce C ].
+Implicit Arguments ga_functor_monoidal [ K ce C ].