projects
/
coq-categories.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
9acb9b7
)
remove reliance on General.v
author
Adam Megacz
<megacz@cs.berkeley.edu>
Wed, 6 Apr 2011 04:48:06 +0000
(
04:48
+0000)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Wed, 6 Apr 2011 04:48:06 +0000
(
04:48
+0000)
12 files changed:
src/Algebras_ch4.v
patch
|
blob
|
history
src/Categories_ch1_3.v
patch
|
blob
|
history
src/CoEqualizers_ch3_4.v
patch
|
blob
|
history
src/Coherence_ch7_8.v
patch
|
blob
|
history
src/Enrichment_ch2_8.v
patch
|
blob
|
history
src/EpicMonic_ch2_1.v
patch
|
blob
|
history
src/Equalizers_ch3_3.v
patch
|
blob
|
history
src/EquivalentCategories_ch7_8.v
patch
|
blob
|
history
src/FreydCategories.v
patch
|
blob
|
history
src/Functors_ch1_4.v
patch
|
blob
|
history
src/Isomorphisms_ch1_5.v
patch
|
blob
|
history
src/Main.v
patch
|
blob
|
history
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.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
(* very handy *)
(*
(* very handy *)
(*
@@
-17,7
+16,7
@@
Fixpoint listOfTypesToType (args:list Type)(ret:Type) : Type :=
| a::b => a -> listOfTypesToType b ret
end.
*)
| a::b => a -> listOfTypesToType b ret
end.
*)
-
+(*
Section Algebras.
Local Notation "a :: b" := (vec_cons a b).
Section Algebras.
Local Notation "a :: b" := (vec_cons a b).
@@
-242,5
+241,5
@@
Definition AMCat_from_MCat `(C:MCat V) : AMCat.
*)
End Algebras.
*)
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.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
(* definition 1.1 *)
Class Category
(* 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.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
(******************************************************************************)
(* Chapter 3.4: CoEqualizers *)
(******************************************************************************)
(* 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.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
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.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
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.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
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.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
(******************************************************************************)
(* Chapter 3.3: Equalizers *)
(******************************************************************************)
(* 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.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
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.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
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.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
(******************************************************************************)
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.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
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.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.