diff options
| author | Nickolai Zeldovich | 2014-09-16 14:52:03 +0000 |
|---|---|---|
| committer | Pierre Boutillier | 2014-10-28 09:09:56 +0100 |
| commit | 1545317ea8b6e7ca4965f06f00bc524d5af1ef47 (patch) | |
| tree | 0c40de308bd1e92dd14b859363f48df8e43c17a8 /dev | |
| parent | 2d88f205592d279bc7a57e0901522214770c2948 (diff) | |
Haskell extraction: put unsafeCoerce type declaration later
When Haskell extraction requires magic type coersion, Coq produces
the following code:
unsafeCoerce :: a -> b
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
import qualified IOExts
unsafeCoerce = IOExts.unsafeCoerce
#endif
GHC version 7.6.3 does not allow imports after a type declaration,
and produces this error:
xx.hs:20:1: parse error on input `import'
(referring to the first import statement above). This patch moves
the unsafeCoerce type declaration to just after the import statement,
fixing this compile error.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions
