X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeductionCategory.v;h=9360bfa6eb8eaa9403ae095f6ae4ff6c4884a43c;hp=7ac59b33ee5275d1e189142f2301b64c34e45f75;hb=034f7e7856bebbbcb3c83946aa603c640b17f3bb;hpb=64d416692bda1d36c33b5efa245d46dcf546ad4a

diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v
index 7ac59b3..9360bfa 100644
--- a/src/NaturalDeductionCategory.v
+++ b/src/NaturalDeductionCategory.v
@@ -72,7 +72,7 @@ Section Judgments_Category.
       setoid_rewrite <- ndr_prod_preserves_comp.
       apply (ndr_builtfrom_structural (f;;g)); auto.
     Defined.
-  Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (fun x y => x,,y) :=
+  Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (@T_Branch (??Judgment)) :=
     { bin_first  := jud_first
     ; bin_second := jud_second }.
 
@@ -136,9 +136,9 @@ Section Judgments_Category.
   ; pmon_assoc_ll := jud_mon_assoc_ll
   }.
     unfold functor_fobj; unfold fmor; simpl;
-      apply Build_Pentagon; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto.
+      apply Build_Pentagon; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto 10.
     unfold functor_fobj; unfold fmor; simpl;
-      apply Build_Triangle; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto.
+      apply Build_Triangle; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto 10.
     intros; unfold eqv; simpl; auto; reflexivity.
     intros; unfold eqv; simpl; auto; reflexivity.
     intros; unfold eqv; simpl; apply Judgments_Category_Commutative.