remove reliance on General.v

diff --git a/src/Algebras_ch4.v b/src/Algebras_ch4.v
index b7f58d9..24e94bd 100644 (file)
--- 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.
-
+*)
 

diff --git a/src/Categories_ch1_3.v b/src/Categories_ch1_3.v
index e0a5838..f5786ee 100644 (file)
--- a/src/Categories_ch1_3.v
+++ b/src/Categories_ch1_3.v
@@ -4,7 +4,6 @@
 
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 
 (* definition 1.1 *)
 Class Category

diff --git a/src/CoEqualizers_ch3_4.v b/src/CoEqualizers_ch3_4.v
index a56bb4d..c60a9b6 100644 (file)
--- a/src/CoEqualizers_ch3_4.v
+++ b/src/CoEqualizers_ch3_4.v
@@ -1,6 +1,5 @@
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 
 (******************************************************************************)
 (* Chapter 3.4: CoEqualizers                                                  *)

diff --git a/src/Coherence_ch7_8.v b/src/Coherence_ch7_8.v
index d683b90..2d5f689 100644 (file)
--- a/src/Coherence_ch7_8.v
+++ b/src/Coherence_ch7_8.v
@@ -1,6 +1,5 @@
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/Enrichment_ch2_8.v b/src/Enrichment_ch2_8.v
index 87d9aa0..2fe7d58 100644 (file)
--- a/src/Enrichment_ch2_8.v
+++ b/src/Enrichment_ch2_8.v
@@ -1,6 +1,5 @@
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/EpicMonic_ch2_1.v b/src/EpicMonic_ch2_1.v
index bc39509..80d95b8 100644 (file)
--- a/src/EpicMonic_ch2_1.v
+++ b/src/EpicMonic_ch2_1.v
@@ -1,6 +1,5 @@
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/Equalizers_ch3_3.v b/src/Equalizers_ch3_3.v
index b4878d5..20b9442 100644 (file)
--- a/src/Equalizers_ch3_3.v
+++ b/src/Equalizers_ch3_3.v
@@ -1,6 +1,5 @@
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 
 (******************************************************************************)
 (* Chapter 3.3: Equalizers                                                    *)

diff --git a/src/EquivalentCategories_ch7_8.v b/src/EquivalentCategories_ch7_8.v
index 6ed769f..db7f76c 100644 (file)
--- a/src/EquivalentCategories_ch7_8.v
+++ b/src/EquivalentCategories_ch7_8.v
@@ -4,7 +4,6 @@
 
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/FreydCategories.v b/src/FreydCategories.v
index 9ea39e0..5f0e1c8 100644 (file)
--- a/src/FreydCategories.v
+++ b/src/FreydCategories.v
@@ -4,7 +4,6 @@
 
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

diff --git a/src/Functors_ch1_4.v b/src/Functors_ch1_4.v
index 0d7f401..ee644ae 100644 (file)
--- a/src/Functors_ch1_4.v
+++ b/src/Functors_ch1_4.v
@@ -1,6 +1,5 @@
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 Require Import Categories_ch1_3.
 
 (******************************************************************************)

diff --git a/src/Isomorphisms_ch1_5.v b/src/Isomorphisms_ch1_5.v
index 65eaf46..372ad43 100644 (file)
--- a/src/Isomorphisms_ch1_5.v
+++ b/src/Isomorphisms_ch1_5.v
@@ -1,6 +1,5 @@
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 

diff --git a/src/Main.v b/src/Main.v
index de30773..2a054b7 100644 (file)
--- a/src/Main.v
+++ b/src/Main.v
@@ -1,6 +1,5 @@
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.