X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FMain.v;h=962ed6d89328cf710dba12a61ceeecfe670987dc;hb=a0b31d2cc2b6cf7184efe4ff01ad682749f779ad;hp=2653fb8ed39e29046261b21613e6f9537b97c46b;hpb=ff3003c261295c60d367580b6700396102eb5a9c;p=coq-categories.git

diff --git a/src/Main.v b/src/Main.v
index 2653fb8..962ed6d 100644
--- a/src/Main.v
+++ b/src/Main.v
@@ -27,7 +27,7 @@ Require Import Coherence_ch7_8.
 Require Import MonoidalCategories_ch7_8.
 
 Require Import Exponentials_ch6.
-Require Import CategoryOfCategories_ch7_1.
+(*Require Import CategoryOfCategories_ch7_1.*)
 Require Import Yoneda_ch8.
 Require Import Adjoints_ch9.
 
@@ -35,7 +35,7 @@ Require Import Adjoints_ch9.
 (*Require Import CoqCategory.*)
 (*Require Import NaturalDeduction.*)
 (*Require Import NaturalDeductionCategories.*)
-(*Require Import CartesianEnrichmentsHaveMonoidalRepresentableFunctors.*)
+(*Require Import CartesianEnrichmentsHaveMonoidalHomFunctors.*)
 (*Require Import Reification.*)
 (*Require Import GeneralizedArrow.*)
 (*Require Import ReificationFromGArrow.*)