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

diff --git a/src/All.v b/src/All.v
index 52bfa4a..9443bbb 100644
--- a/src/All.v
+++ b/src/All.v
@@ -1,86 +1,9 @@
-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.
-
+Require Import ExtractionMain.
+Require Import HaskProgrammingLanguage.
+Require Import PCF.
+Require Import HaskFlattener.
+Require Import ProgrammingLanguageArrow.
+Require Import ProgrammingLanguageReification.
+Require Import ProgrammingLanguageFlattening.
+Require Import ReificationsIsomorphicToGeneralizedArrows.