From ffc135337b479349a9e94c0da0a87531cf0684fa Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 5 Jan 2016 19:48:32 +0100
Subject: Disable warning 31 when generating coqtop from coqmktop.

In OCaml 3.x, the toploop of OCaml was accessible from toplevellib.cma. In
OCaml 4.x, it was replaced by compiler-libs. However, linking with
compiler-libs produces a warning (fatal with OCaml 4.03) as soon as we have a
file named errors.ml or lexer.ml...

The only satisfactory solution seems to be to "pack" compiler libs. But it is
not done currently in the OCaml distribution, and implementing it in coqmktop
at this point would be too risky. So for now, I am disabling the warning until
we hear from the OCaml team. In principle, this clash of modules names can
break OCaml's type safety, so we are living dangerously.
---
 tools/coqmktop.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index be796e6956..e29cf60e36 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -280,7 +280,7 @@ let main () =
     (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper.
        - With the coq .cma, we MUST use the -linkall option. *)
     let args =
-      "-linkall" :: "-rectypes" :: flags @ copts @ options @
+      "-linkall" :: "-rectypes" :: "-w" :: "-31" :: flags @ copts @ options @
       (std_includes basedir) @ tolink @ [ main_file ] @ topstart
     in
     if !echo then begin
-- 
cgit v1.2.3