X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeductionCategory.v;h=0a82aa2ccde9e84c394de5795ff441616885cad7;hp=0a413e75ff8ccb8c7588e6a10790a5db62705d3e;hb=d1a4d10de986d774d3cfb10348036cb60bc80277;hpb=e83fd6f566ed0a7aaff19d67c2c2b64d08f98f7c

diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v
index 0a413e7..0a82aa2 100644
--- a/src/NaturalDeductionCategory.v
+++ b/src/NaturalDeductionCategory.v
@@ -20,9 +20,11 @@ Require Import Enrichment_ch2_8.
 Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
-Require Import MonoidalCategories_ch7_8.
 Require Import Coherence_ch7_8.
 Require Import InitialTerminal_ch2_2.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
+Require Import MonoidalCategories_ch7_8.
 
 Open Scope nd_scope.
 Open Scope pf_scope.