diff options
| author | Nickolai Zeldovich | 2015-03-28 08:19:05 -0400 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-04-02 16:51:30 +0200 |
| commit | f10a4ac8e58917f0d9b11458465a963a562aa582 (patch) | |
| tree | 869bf59c4919689fd0bbc40058c62751906ce07d /dev | |
| parent | 3d8c7b24ac97e8d714f343cc0e49e8dff9c90aaf (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 'dev')
0 files changed, 0 insertions, 0 deletions
