X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeductionCategory.v;h=d721a9708045971b9cf24a8061edd1ba09231b33;hp=7ac59b33ee5275d1e189142f2301b64c34e45f75;hb=77e8c70f4fd7a32db036fee5884a98208d450de2;hpb=64d416692bda1d36c33b5efa245d46dcf546ad4a diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v index 7ac59b3..d721a97 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 }.