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.
---
 vernac/metasyntax.ml | 4 ++--
 vernac/ppvernac.ml   | 2 +-
 vernac/search.ml     | 2 +-
 vernac/topfmt.ml     | 4 ++--
 4 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'vernac')

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 90892feb13..e754ead5dd 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -519,7 +519,7 @@ let read_recursive_format sl fmt =
     let sl = skip_var_in_recursive_format fmt in
     try split_format_at_ldots [] sl with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in
   let rec get_tail = function
-    | (loc,a) :: sepfmt, (_,b) :: fmt when Pervasives.(=) a b -> get_tail (sepfmt, fmt) (* FIXME *)
+    | (loc,a) :: sepfmt, (_,b) :: fmt when (=) a b -> get_tail (sepfmt, fmt) (* FIXME *)
     | [], tail -> skip_var_in_recursive_format tail
     | (loc,_) :: _, ([] | (_,UnpTerminal _) :: _)-> error_not_same ?loc ()
     | _, (loc,_)::_ -> error_not_same ?loc () in
@@ -953,7 +953,7 @@ let join_auxiliary_recursive_types recvars etyps =
     | None, None -> typs
     | Some _, None -> typs
     | None, Some ytyp -> (x,ytyp)::typs
-    | Some xtyp, Some ytyp when Pervasives.(=) xtyp ytyp -> typs (* FIXME *)
+    | Some xtyp, Some ytyp when (=) xtyp ytyp -> typs (* FIXME *)
     | Some xtyp, Some ytyp ->
 	user_err 
 	  (strbrk "In " ++ Id.print x ++ str " .. " ++ Id.print y ++
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 78112d9dc4..e676fe94db 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -371,7 +371,7 @@ open Pputils
     | (c,(idl,t))::l ->
       match factorize l with
         | (xl,((c', t') as r))::l'
-            when (c : bool) == c' && Pervasives.(=) t t' ->
+            when (c : bool) == c' && (=) t t' ->
           (* FIXME: we need equality on constr_expr *)
           (idl@xl,r)::l'
         | l' -> (idl,(c,t))::l'
diff --git a/vernac/search.ml b/vernac/search.ml
index 101a578587..964d01260b 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -148,7 +148,7 @@ module ConstrPriority = struct
     -(3*(num_symbols t) + size t)
 
   let compare (_,_,_,p1) (_,_,_,p2) =
-    Pervasives.compare p1 p2
+    pervasives_compare p1 p2
 end
 
 module PriorityQueue = Heap.Functional(ConstrPriority)
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 7644f4c5b6..046defc26b 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -329,8 +329,8 @@ let init_terminal_output ~color =
       Format.pp_set_print_tags !std_ft true;
       Format.pp_set_print_tags !err_ft true
     end;
-  Format.pp_set_formatter_tag_functions !std_ft (tag_handler !std_ft);
-  Format.pp_set_formatter_tag_functions !err_ft (tag_handler !err_ft)
+  Format.pp_set_formatter_tag_functions !std_ft (tag_handler !std_ft) [@warning "-3"];
+  Format.pp_set_formatter_tag_functions !err_ft (tag_handler !err_ft) [@warning "-3"]
 
 (* Rules for emacs:
    - Debug/info: emacs_quote_info
-- 
cgit v1.2.3