aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-07-04 18:05:01 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-07-04 18:05:01 +0000
commit9b01effde4e3fb6d7e9cf54ed1ede6362f77ea72 (patch)
tree7c4207d3b01fd2fca8078bbbd4a4a1f1ddee9291
parent7382948497f1ae935bd2b16596e468605a3d8033 (diff)
Extraction: in haskell, type signatures for __ and unsafeCoerce (fix #2552)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14257 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--plugins/extraction/haskell.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index e23e3bf79..b51a957af 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -45,6 +45,7 @@ let preamble mod_name used_modules usf =
(if used_modules = [] then mt () else fnl ()) ++
(if not usf.magic then mt ()
else str "\
+\nunsafeCoerce :: a -> b\
\n#ifdef __GLASGOW_HASKELL__\
\nimport qualified GHC.Base\
\nunsafeCoerce = GHC.Base.unsafeCoerce#\
@@ -55,7 +56,8 @@ let preamble mod_name used_modules usf =
\n#endif" ++ fnl2 ())
++
(if not usf.mldummy then mt ()
- else str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
+ else str "__ :: any" ++ fnl () ++
+ str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
let pp_abst = function
| [] -> (mt ())