diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-01-05 19:48:32 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-01-05 22:58:19 +0100 |
| commit | ffc135337b479349a9e94c0da0a87531cf0684fa (patch) | |
| tree | 2571773259a297851a458470ff9d869eb642ecb6 /library/goptions.mli | |
| 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.
Diffstat (limited to 'library/goptions.mli')
0 files changed, 0 insertions, 0 deletions