From 2403342ad32f12dd56a82ce575dd2d35d91f545a Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Wed, 6 Apr 2011 04:48:06 +0000 Subject: [PATCH] remove reliance on General.v --- src/Algebras_ch4.v | 5 ++--- src/Categories_ch1_3.v | 1 - src/CoEqualizers_ch3_4.v | 1 - src/Coherence_ch7_8.v | 1 - src/Enrichment_ch2_8.v | 1 - src/EpicMonic_ch2_1.v | 1 - src/Equalizers_ch3_3.v | 1 - src/EquivalentCategories_ch7_8.v | 1 - src/FreydCategories.v | 1 - src/Functors_ch1_4.v | 1 - src/Isomorphisms_ch1_5.v | 1 - src/Main.v | 1 - 12 files changed, 2 insertions(+), 14 deletions(-) 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. - +*) diff --git a/src/Categories_ch1_3.v b/src/Categories_ch1_3.v index e0a5838..f5786ee 100644 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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. -- 1.7.10.4