src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML
author Manuel Eberl <eberlm@in.tum.de>
Tue, 19 Jan 2016 11:19:25 +0100
changeset 62201 eca7b38c8ee5
parent 62058 1cfd5d604937
permissions -rw-r--r--
Added approximation of powr to NEWS/CONTRIBUTORS
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62058
1cfd5d604937 updated headers;
wenzelm
parents: 61925
diff changeset
     1
(*  Title:      Pure/RAW/ml_compiler_parameters_polyml-5.6.ML
60745
d86b4cd0f1ec clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
d86b4cd0f1ec clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
diff changeset
     3
61794
4c232a2ddeab discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6;
wenzelm
parents: 60745
diff changeset
     4
Additional ML compiler parameters for Poly/ML 5.6, or later.
60745
d86b4cd0f1ec clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
diff changeset
     5
*)
d86b4cd0f1ec clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
diff changeset
     6
d86b4cd0f1ec clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
diff changeset
     7
structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
d86b4cd0f1ec clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
diff changeset
     8
struct
d86b4cd0f1ec clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
diff changeset
     9
d86b4cd0f1ec clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
diff changeset
    10
fun debug b = [PolyML.Compiler.CPDebug b];
d86b4cd0f1ec clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
diff changeset
    11
d86b4cd0f1ec clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
wenzelm
parents:
diff changeset
    12
end;