aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-10-09 16:12:26 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-10-10 10:47:58 +0200
commit1d8725b59309c2c9f870eb52a2daebe87ed9ad5b (patch)
tree5f7beb8ea5b420cbbcbad414e6f216b34d08b464 /config
parent406717ce786a70e64b9043db45dd5a2add68f817 (diff)
[flambda] [native] Pass `-Oclassic` to the native compiler.
This seems a safe choice as of today, but more advanced users would like to tweak it, or we could even refine it by a configure option if desired.
Diffstat (limited to 'config')
-rw-r--r--config/coq_config.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 885b3ef4c..8bc044c3a 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -49,6 +49,7 @@ val vmbyteflags : string list (* -custom/-dllib -lcoqrun *)
val version : string (* version number of Coq *)
val caml_version : string (* OCaml version used to compile Coq *)
+val caml_version_nums : int list (* OCaml version used to compile Coq by components *)
val date : string (* release date *)
val compile_date : string (* compile date *)
val vo_magic_number : int