aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index 04b04979d..caef75271 100644
--- a/configure.ml
+++ b/configure.ml
@@ -510,6 +510,8 @@ let camltag = match caml_version_list with
| x::y::_ -> "OCAML"^x^y
| _ -> assert false
+let coq_warn_flag =
+ if caml_version_nums > [4;2;3] then "-w -3-52-56" else ""
(** * CamlpX configuration *)
@@ -1128,7 +1130,7 @@ let write_makefile f =
pr "CAMLHLIB=%S\n\n" camllib;
pr "# Caml link command and Caml make top command\n";
pr "# Caml flags\n";
- pr "CAMLFLAGS=-rectypes %s\n" coq_annotate_flag;
+ pr "CAMLFLAGS=-rectypes %s %s\n" coq_annotate_flag coq_warn_flag;
pr "# User compilation flag\n";
pr "USERFLAGS=\n\n";
pr "# Flags for GCC\n";