X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FAlgebras_ch4.v;h=24e94bdad98be6478d4ea11607cb3e2c4c775058;hp=b7f58d90ab23597aab85bdd2058e9bd1ff4a5aac;hb=2403342ad32f12dd56a82ce575dd2d35d91f545a;hpb=9acb9b7b4ed12543e54c39c82d7b0f34d04d0207

diff --git a/src/Algebras_ch4.v b/src/Algebras_ch4.v
index b7f58d9..24e94bd 100644
--- a/src/Algebras_ch4.v
+++ b/src/Algebras_ch4.v
@@ -7,7 +7,6 @@
 
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 
 (* very handy *)
 (*
@@ -17,7 +16,7 @@ Fixpoint listOfTypesToType (args:list Type)(ret:Type) : Type :=
   | a::b => a -> listOfTypesToType b ret
   end.
 *)
-
+(*
 Section Algebras.
 
 Local Notation "a :: b" := (vec_cons a b).
@@ -242,5 +241,5 @@ Definition AMCat_from_MCat `(C:MCat V) : AMCat.
 
 *)
 End Algebras.
-
+*)