X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneralizedArrowFromReification.v;h=b5e31479155ba0ca65f63601ffd0dbd87634f1b7;hp=9ff0d4df8bd35789d076ed1ba5d5282109dbe1a7;hb=e539b49ae3148ab1967b5ea0709734171180b86d;hpb=4e5aa4bcc6024aa7add9c1bf1c2ad9fd2a6a3685

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index 9ff0d4d..b5e3147 100644
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -916,7 +916,7 @@ Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0]
     apply (fmor_respects (-⋉ F b)).
     apply iso_comp2.
     Qed.
-*)
+
   Lemma cancell_coherent (b:enr_v K) :
    #(pmon_cancell(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
    (#(iso_id (enr_c_i C)) ⋉ garrow_functor b >>>
@@ -1162,7 +1162,7 @@ Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0]
     apply assoc_coherent.
     Defined.
 
-  Definition garrow_from_reification : GeneralizedArrow K CM :=
+  Definition garrow_from_reification : GeneralizedArrow K C :=
     {| ga_functor_monoidal := garrow_monoidal
      ; ga_host_lang_pure   := reification_host_lang_pure _ _ _ reification
     |}.