aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_syntax.ml
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/syntax/string_syntax.ml
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/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions