separate HaskProofStratified into PCF.v, HaskProgrammingLanguage.v, and HaskFlattener...

[coq-hetmet.git] / src / All.v

diff --git a/src/All.v b/src/All.v
index b42d175..9443bbb 100644 (file)
--- a/src/All.v
+++ b/src/All.v
@@ -1,89 +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 WeakFunctorCategory.
-Require Import SmallSMMEs.
-Require Import ReificationCategory.
-Require Import GeneralizedArrowCategory.
-Require Import ReificationsAndGeneralizedArrows.
+Require Import ExtractionMain.
+Require Import HaskProgrammingLanguage.
+Require Import PCF.
+Require Import HaskFlattener.
+Require Import ProgrammingLanguageArrow.
+Require Import ProgrammingLanguageReification.
+Require Import ProgrammingLanguageFlattening.
 Require Import ReificationsIsomorphicToGeneralizedArrows.
 
-Require Import HaskProofCategory.
-Require Import ProgrammingLanguage.
-
-(* very slow! *)
-Require Import FreydCategories.
-Require Import Arrows.
-
-