diff options
| author | Maxime Dénès | 2016-01-05 19:48:32 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-01-05 22:58:19 +0100 |
| commit | ffc135337b479349a9e94c0da0a87531cf0684fa (patch) | |
| tree | 2571773259a297851a458470ff9d869eb642ecb6 | |
| parent | 64487121a35628512c1bd1b4e7039132f84ab270 (diff) | |
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.
| -rw-r--r-- | tools/coqmktop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |