aboutsummaryrefslogtreecommitdiff
path: root/plugins/pluginsbyte.itarget
diff options
context:
space:
mode:
authorNickolai Zeldovich2015-03-28 08:19:05 -0400
committerGuillaume Melquiond2015-04-02 16:51:30 +0200
commitf10a4ac8e58917f0d9b11458465a963a562aa582 (patch)
tree869bf59c4919689fd0bbc40058c62751906ce07d /plugins/pluginsbyte.itarget
parent3d8c7b24ac97e8d714f343cc0e49e8dff9c90aaf (diff)
Define Any in Haskell extraction when Tunknown is used.
Commit 84c2433a introduced the Any type alias as the Haskell extracted version of MiniML's Tunknown. However, the code to define the Any type alias was generated conditional on usf.magic. As it turns out, sometimes Tunknown appears even if usf.magic is false (i.e., even if MLmagic does not appear anywhere in the AST). This produced Haskell code that would not compile; e.g.: % coqtop Coq < Extraction Language Haskell. Coq < Extraction Library Datatypes. The file Datatypes.hs has been created by extraction. % ghc Datatypes.hs [1 of 1] Compiling Datatypes ( Datatypes.hs, Datatypes.o ) Datatypes.hs:261:17: Not in scope: type constructor or class `Any' Datatypes.hs:261:24: Not in scope: type constructor or class `Any' The fix is straightforward: produce the code that defines the Any type alias if usf.tunknown is true.
Diffstat (limited to 'plugins/pluginsbyte.itarget')
0 files changed, 0 insertions, 0 deletions