change name of string-extraction placeholder

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 3179cdb..041ca7e 100644 (file)
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -35,13 +35,6 @@ import qualified GHC.Base
 import qualified System.IO
 import qualified System.IO.Unsafe
 
-{-  -- used for extracting strings WITHOUT the patch for Coq
-bin2ascii =
-  (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
-     let f b i = if b then 1 `shiftL` i else 0
-     in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7))
--}
-
 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
 getTyConTyVars tc =
   if TyCon.isFunTyCon tc
@@ -159,7 +152,7 @@ coreCoercionToWeakCoercion c =
               (TyCon.CoCsel2 , []        ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
               (TyCon.CoCselR , []        ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
               (TyCon.CoInst  , []        ) -> Prelude.error "CoInst  is not in post-publication-appendix SystemFC1"
---              (TyCon.CoAxiom , []        ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
+              (TyCon.CoAxiom , []        ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
               _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
   _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 --  TypeRep.ForAllTy v t   -> WCoAll  (Prelude.error "FIXME") (coreTypeToWeakType t)
@@ -191,3 +184,10 @@ trace msg x = System.IO.Unsafe.unsafePerformIO $
 trace msg x = System.IO.Unsafe.unsafePerformIO $
                 (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)
 -}
+
+{-  -- used for extracting strings WITHOUT the patch for Coq
+bin2ascii =
+  (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
+     let f b i = if b then 1 `shiftL` i else 0
+     in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7))
+-}

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index dbeb3cc..2f0856f 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -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".