X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=ba0c2418490cdefd3e1338571ecd1fead1de7f8d;hp=2f0856fc199537a40117c4f548f473867cc4a812;hb=fd337b235014f43000773eb0d95168d89e93a893;hpb=50747fb9b9a44a24ea7a29b8703706386f6cd092

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 2f0856f..ba0c241 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -35,13 +35,11 @@ Require Import HaskWeakToCore.
 Require Import HaskProofToStrong.
 
 Require Import ProgrammingLanguage.
-
 Require Import HaskProofCategory.
-(*
-Require Import HaskStrongCategory.
-*)
 Require Import ReificationsIsomorphicToGeneralizedArrows.
 
+(*Require Import HaskStrongCategory.*)
+
 Open Scope string_scope.
 Extraction Language Haskell.
 
@@ -228,6 +226,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 +234,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)) (