X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FExtractionMain.v;h=2f0856fc199537a40117c4f548f473867cc4a812;hb=be2a24c17877b3401c3c46bee1436b8ec0bbdaf5;hp=2b65a182ac5efc36942cbd4f67d4449fd03c3b83;hpb=97552c1a6dfb32098d4491951929ab1d4aca96a0;p=coq-hetmet.git

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 2b65a18..2f0856f 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -34,12 +34,13 @@ Require Import HaskStrongToWeak.
 Require Import HaskWeakToCore.
 Require Import HaskProofToStrong.
 
+Require Import ProgrammingLanguage.
+
 Require Import HaskProofCategory.
 (*
 Require Import HaskStrongCategory.
-Require Import ReificationsEquivalentToGeneralizedArrows.
-Require Import ProgrammingLanguage.
 *)
+Require Import ReificationsIsomorphicToGeneralizedArrows.
 
 Open Scope string_scope.
 Extraction Language Haskell.
@@ -61,7 +62,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".
@@ -99,7 +100,8 @@ Section core2proof.
   Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
     match coreVarToWeakVar cv with
       | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
-                          | Error s => Prelude_error ("Error in top-level xi: " +++ s)
+                          | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
+                                                         toString cv+++": " +++ s)
                           | OK    t => t @@ nil
                         end
       | WTypeVar _   => Prelude_error "top-level xi got a type variable"