X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FWeakFunctorCategory.v;h=85ade6128f578b38a7e2872f228f6714a3958900;hp=49a5189fe9bfb820e261bdf265f74cae74302749;hb=e536cc4194f350ed6de5d465bcf53fda650b3d12;hpb=3351499d7cb3d32c8df441426309ec6a1ef2a035;ds=sidebyside

diff --git a/src/WeakFunctorCategory.v b/src/WeakFunctorCategory.v
index 49a5189..85ade61 100644
--- a/src/WeakFunctorCategory.v
+++ b/src/WeakFunctorCategory.v
@@ -192,8 +192,8 @@ Section WeakFunctorCategoryIsomorphism.
         apply q.
         Defined.
 
-    Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE F1 F2.
-      apply Build_IsomorphicCategories.
+    Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE.
+      refine {| ic_f := F1 ; ic_g := F2 |}.
       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
         eapply if_comp.
         apply m1_m2_id.