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

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index dbeb3cc..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.
 
@@ -62,7 +60,7 @@ Extract Inlined Constant string_dec => "(==)".
 Extract Inlined Constant ascii_dec => "(==)".
 
 (* adapted from ExtrOcamlString.v *)
-Extract Inductive ascii => "Char" [ "bin2ascii" ] "bin2ascii'".
+Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
 Extract Constant zero   => "'\000'".
 Extract Constant one    => "'\001'".
 Extract Constant shift  => "shiftAscii".
@@ -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)) (