From dda7d129dba6c90d642cd99cd989e5f13c0eb4b4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 3 Jul 2019 12:54:37 +0200 Subject: [core] [api] Support OCaml 4.08 The changes are large due to `Pervasives` deprecation: - the `Pervasives` module has been deprecated in favor of `Stdlib`, we have opted for introducing a few wrapping functions in `Util` and just unqualified the rest of occurrences. We avoid the shims as in the previous attempt. - a bug regarding partial application have been fixed. - some formatting functions have been deprecated, but previous versions don't include a replacement, thus the warning has been disabled. We may want to clean up things a bit more, in particular w.r.t. modules once we can move to OCaml 4.07 as the minimum required version. Note that there is a clash between 4.08.0 modules `Option` and `Int` and Coq's ones. It is not clear if we should resolve that clash or not, see PR #10469 for more discussion. On the good side, OCaml 4.08.0 does provide a few interesting functionalities, including nice new warnings useful for devs. --- tools/coqdoc/main.ml | 2 +- tools/coqdoc/output.ml | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) (limited to 'tools/coqdoc') diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 1c22efa513..3442ebb731 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -396,7 +396,7 @@ let copy src dst = try let cout = open_out dst in try - while true do Pervasives.output_char cout (input_char cin) done + while true do output_char cout (input_char cin) done with End_of_file -> close_out cout; close_in cin diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 9b7da862a8..02f0290802 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -13,9 +13,9 @@ open Index (*s Low level output *) -let output_char c = Pervasives.output_char !out_channel c +let output_char c = output_char !out_channel c -let output_string s = Pervasives.output_string !out_channel s +let output_string s = output_string !out_channel s let printf s = Printf.fprintf !out_channel s @@ -527,13 +527,13 @@ module Html = struct let header () = if !header_trailer then if !header_file_spec then - let cin = Pervasives.open_in !header_file in + let cin = open_in !header_file in try while true do - let s = Pervasives.input_line cin in + let s = input_line cin in printf "%s\n" s done - with End_of_file -> Pervasives.close_in cin + with End_of_file -> close_in cin else begin printf " Pervasives.close_in cin + with End_of_file -> close_in cin else begin if !index && (get_module false) <> "Index" then -- cgit v1.2.3