X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationFromGeneralizedArrow.v;h=730d91de1b9158a58a5d25bcac1b1c4985b47745;hp=1a5fea717e0bf95febb636aa4b1fe0283fe06f63;hb=93ac0d63048027161f816c451a7954fb8a6470c0;hpb=77e8c70f4fd7a32db036fee5884a98208d450de2

diff --git a/src/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v
index 1a5fea7..730d91d 100644
--- a/src/ReificationFromGeneralizedArrow.v
+++ b/src/ReificationFromGeneralizedArrow.v
@@ -26,7 +26,7 @@ Require Import RepresentableStructure_ch7_2.
 Require Import Reification.
 Require Import GeneralizedArrow.
 
-Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) (garrow : GeneralizedArrow K C)
+Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) (garrow : GeneralizedArrow K ce)
  : Reification K ce (enr_c_i ce).
   refine
   {| reification_r         := fun k:K => HomFunctor K k >>>> ga_functor garrow