diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-07-10 14:57:20 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-07-10 14:57:20 +0200 |
| commit | 6e1a5ce6c6dc820ca9030261dfb2b7a0e4919642 (patch) | |
| tree | 2cb3f8125e4fa3064eb996cd349ece73b689b78d /lib/Camlcoq.ml | |
| parent | 380a8489a882fc3eab02aa3d0cc03a2aa8078044 (diff) | |
| download | compcert-kvx-6e1a5ce6c6dc820ca9030261dfb2b7a0e4919642.tar.gz compcert-kvx-6e1a5ce6c6dc820ca9030261dfb2b7a0e4919642.zip | |
Compatibility with OCaml 4.07 (#241)
OCaml 4.07 introduces a Float submodule of the Stdlib
opened-by-default compilation unit. CompCert's Float compilation unit
also has a Float submodule. This triggers warning 44 when Floats is
opened. The workaround is just to silence the warning with `open! Floats`.
Closes: #241
Diffstat (limited to 'lib/Camlcoq.ml')
| -rw-r--r-- | lib/Camlcoq.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 5c25796e..d94e3582 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -20,7 +20,7 @@ open BinNums open BinNat open BinInt open BinPos -open Floats +open! Floats (* Coq's [nat] type and some of its operations *) |