X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=2f0856fc199537a40117c4f548f473867cc4a812;hp=05d059a81b4fc4c78b73ab23d3868cac0fc6cf60;hb=9444d329585e0dc3400a3bbb8155900f9ad62b92;hpb=20a9b4934a97e6801d6785ac940f771cb74a8cc1

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 05d059a..2f0856f 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -40,7 +40,7 @@ Require Import HaskProofCategory.
 (*
 Require Import HaskStrongCategory.
 *)
-Require Import ReificationsEquivalentToGeneralizedArrows.
+Require Import ReificationsIsomorphicToGeneralizedArrows.
 
 Open Scope string_scope.
 Extraction Language Haskell.
@@ -62,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".