author | wenzelm |
Fri Jul 17 16:43:53 2015 +0200 (2015-07-17) | |
changeset 60745 | d86b4cd0f1ec |
permissions | -rw-r--r-- |
wenzelm@60745 | 1 |
(* Title: Pure/ML/ml_compiler_parameters.ML |
wenzelm@60745 | 2 |
Author: Makarius |
wenzelm@60745 | 3 |
|
wenzelm@60745 | 4 |
Additional ML compiler parameters for Poly/ML. |
wenzelm@60745 | 5 |
*) |
wenzelm@60745 | 6 |
|
wenzelm@60745 | 7 |
signature ML_COMPILER_PARAMETERS = |
wenzelm@60745 | 8 |
sig |
wenzelm@60745 | 9 |
val debug: bool -> PolyML.Compiler.compilerParameters list |
wenzelm@60745 | 10 |
end; |
wenzelm@60745 | 11 |
|
wenzelm@60745 | 12 |
structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS = |
wenzelm@60745 | 13 |
struct |
wenzelm@60745 | 14 |
|
wenzelm@60745 | 15 |
fun debug _ = []; |
wenzelm@60745 | 16 |
|
wenzelm@60745 | 17 |
end; |