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

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