X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FAll.v;h=25fa85d1ed80a049e112c10489488ca814f0a1a0;hp=d9f1d16faa0f3d7f5c467cc8454bc32c5008f3d2;hb=916f33924e493c9be8290d0aadc35cf85d6899af;hpb=c6086660ba8a453a62ce7c248c2dabac1627e94b

diff --git a/src/All.v b/src/All.v
index d9f1d16..25fa85d 100644
--- a/src/All.v
+++ b/src/All.v
@@ -1,90 +1,7 @@
-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 WeakFunctorCategory.
-Require Import SmallSMMEs.
-Require Import ReificationCategory.
-Require Import GeneralizedArrowCategory.
-Require Import ReificationsAndGeneralizedArrows.
+Require Import ExtractionMain.
+Require Import ProgrammingLanguageGeneralizedArrow.
+Require Import ProgrammingLanguageFlattening.
+Require Import ProgrammingLanguageArrow.
+Require Import ProgrammingLanguageReification.
 Require Import ReificationsIsomorphicToGeneralizedArrows.
 
-Require Import HaskProofStratified.
-Require Import HaskProofFlattener.
-Require Import ProgrammingLanguage.
-
-(* very slow! *)
-Require Import FreydCategories.
-Require Import Arrows.
-
-