X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FAll.v;fp=src%2FAll.v;h=52bfa4acb60afb197c1964c01d1845e53b02449c;hp=0000000000000000000000000000000000000000;hb=2202d864c3a2779a33f3f7d6c411d2d16770073e;hpb=0aa54e44e3ecbc2ad27ce793ea66ce6aad132776

diff --git a/src/All.v b/src/All.v
new file mode 100644
index 0000000..52bfa4a
--- /dev/null
+++ b/src/All.v
@@ -0,0 +1,86 @@
+Require Import Preamble.
+Require Import General.
+
+Require Import HaskKinds.
+Require Import HaskLiteralsAndTyCons.
+
+Require Import HaskCoreVars.
+Require Import HaskCoreTypes.
+Require Import HaskCore.
+
+Require Import HaskWeakTypes.
+Require Import HaskWeakVars.
+Require Import HaskWeak.
+
+Require Import HaskCoreToWeak.
+
+Require Import HaskStrongTypes.
+Require Import HaskStrong.
+
+Require Import NaturalDeduction.
+Require Import NaturalDeductionToLatex.
+
+Require Import HaskProof.
+
+Require Import HaskProofToStrong.
+Require Import HaskStrongToWeak.
+Require Import HaskWeakToCore.
+(*Require Import HaskWeakToStrong.*)
+Require Import HaskStrongToProof.
+(*Require Import HaskProofToLatex.*)
+
+(*Require Import HaskStrongCategory.*)
+(*Require Import Extraction.*)
+
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import OppositeCategories_ch1_6_2.
+Require Import SliceCategories_ch1_6_4.
+
+Require Import EpicMonic_ch2_1.
+Require Import InitialTerminal_ch2_2.
+Require Import SectionRetract_ch2_4.
+
+Require Import Equalizers_ch3_3.
+Require Import CoEqualizers_ch3_4.
+
+Require Import Algebras_ch4.
+
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import FunctorCategories_ch7_7.
+
+Require Import Subcategories_ch7_1.
+
+Require Import Coherence_ch7_8.
+Require Import MonoidalCategories_ch7_8.
+
+Require Import Enrichment_ch2_8.
+Require Import RepresentableStructure_ch7_2.
+
+Require Import Yoneda_ch8.
+(*Require Import Exponentials_ch6.*)
+
+(*Require Import CategoryOfCategories_ch7_1.*)
+(*Require Import Adjoints_ch9.*)
+
+Require Import NaturalDeductionCategory.
+
+Require Import Reification.
+Require Import GeneralizedArrow.
+Require Import GeneralizedArrowFromReification.
+Require Import ReificationFromGeneralizedArrow.
+Require Import ReificationCategory.
+Require Import GeneralizedArrowCategory.
+Require Import ReificationsEquivalentToGeneralizedArrows.
+
+Require Import HaskProofCategory.
+Require Import ProgrammingLanguage.
+
+(* very slow! *)
+Require Import FreydCategories.
+Require Import Arrows.
+
+