replace UJudg with Arrange

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

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index dbeb3cc..ba0c241 100644 (file)
--- 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)) (