X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=6ae977dc74611b5887175a224454d10eb701c464;hp=2f0856fc199537a40117c4f548f473867cc4a812;hb=e3e2ce9cb83acdd8191049b4e9bd3d4fcf6a4db4;hpb=d51e5dc2fcc6b6c7d40aa45397925dc3444c3dbb

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 2f0856f..6ae977d 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -36,12 +36,14 @@ Require Import HaskProofToStrong.
 
 Require Import ProgrammingLanguage.
 
+Require Import HaskProofFlattener.
+Require Import HaskProofStratified.
 Require Import HaskProofCategory.
-(*
-Require Import HaskStrongCategory.
-*)
+
 Require Import ReificationsIsomorphicToGeneralizedArrows.
 
+(*Require Import HaskStrongCategory.*)
+
 Open Scope string_scope.
 Extraction Language Haskell.
 
@@ -228,6 +230,7 @@ Section core2proof.
       apply t.
       Defined.
 
+(*
     Definition env := ★::nil.
     Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
     Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
@@ -235,13 +238,13 @@ Section core2proof.
       eapply nd_comp.
       eapply nd_rule.
       apply RVar.
-      eapply nd_rule.
-      eapply (RURule _ _ _ _ (RuCanL _ _)) .
+      eapply nd_rule
+      eapply (RArrange _ _ _ _ (RuCanL _ _)) .
       eapply nd_rule.
       eapply RLam.
       Defined.
 
-(*
+
     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
     addErrorMessage ("input CoreSyn: " +++ toString ce)
     (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (