uncomment FullImage development

[coq-categories.git] / src / Algebras_ch4.v

diff --git a/src/Algebras_ch4.v b/src/Algebras_ch4.v
index b7f58d9..c18634d 100644 (file)
--- a/src/Algebras_ch4.v
+++ b/src/Algebras_ch4.v
@@ -6,8 +6,7 @@
 (******************************************************************************)
 
 Generalizable All Variables.
-Require Import Preamble.
-Require Import General.
+Require Import Notations.
 
 (* 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.
-
+*)