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

diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v
index d721a97..9360bfa 100644
--- a/src/NaturalDeductionCategory.v
+++ b/src/NaturalDeductionCategory.v
@@ -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.