Merge PR #10471: [core] [api] Support OCaml 4.08

Reviewed-by: SkySkimmer
Ack-by: Zimmi48

53 files changed, 125 insertions, 105 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index f418df3d75..7c9a5c9a31 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -10,7 +10,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2019-07-05-V33"
+  CACHEKEY: "bionic_coq-V2019-07-06-V22"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/INSTALL b/INSTALL
index 0810b0b707..e7a9ea4ab2 100644
--- a/INSTALL
+++ b/INSTALL
@@ -9,7 +9,7 @@ WHAT DO YOU NEED ?
 
    - OCaml (version >= 4.05.0)
      (available at https://ocaml.org/)
-     (This version of Coq has been tested up to OCaml 4.07.0)
+     (This version of Coq has been tested up to OCaml 4.08.0)
 
    - The Num package, which used to be part of the OCaml standard library,
      if you are using an OCaml version >= 4.06.0
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 54d6b4b7c8..e0c4125838 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -67,7 +67,7 @@ jobs:
       opam list
     displayName: 'Install OCaml dependencies'
     env:
-      COMPILER: "4.07.1"
+      COMPILER: "4.08.0"
       FINDLIB_VER: ".1.8.0"
       OPAMYES: "true"
 
diff --git a/checker/analyze.ml b/checker/analyze.ml
index 77e70318dd..e145988b4f 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -395,8 +395,8 @@ end
 module IChannel =
 struct
   type t = in_channel
-  let input_byte = Pervasives.input_byte
-  let input_binary_int = Pervasives.input_binary_int
+  let input_byte = input_byte
+  let input_binary_int = input_binary_int
 end
 
 module IString =
diff --git a/checker/check.ml b/checker/check.ml
index 2840fc9ad6..ecf84fda9c 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -66,7 +66,7 @@ module LibraryOrdered =
   struct
     type t = DirPath.t
     let compare d1 d2 =
-      Pervasives.compare
+      compare
         (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2))
   end
 
@@ -377,7 +377,7 @@ let intern_from_file ~intern_mode (dir, f) =
 let get_deps (dir, f) =
   try LibraryMap.find dir !depgraph
   with Not_found ->
-    let _ = intern_from_file (dir,f) in
+    let _ = intern_from_file ~intern_mode:Dep (dir,f) in
     LibraryMap.find dir !depgraph
 
 (* Read a compiled library and all dependencies, in reverse order.
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index 9448a03f4f..34d748e1cc 100755
--- a/dev/ci/azure-opam.sh
+++ b/dev/ci/azure-opam.sh
@@ -2,7 +2,7 @@
 
 set -e -x
 
-OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c
+OPAM_VARIANT=ocaml-variants.4.08.0+mingw64c
 
 wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz
 tar -xf opam64.tar.xz
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 8b4af9b63f..011c7fbdec 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-07-05-V33"
+# CACHEKEY: "bionic_coq-V2019-07-06-V22"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -22,7 +22,7 @@ RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \
                  antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0
 
 # We need to install OPAM 2.0 manually for now.
-RUN wget https://github.com/ocaml/opam/releases/download/2.0.3/opam-2.0.3-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
+RUN wget https://github.com/ocaml/opam/releases/download/2.0.4/opam-2.0.4-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
 
 # Basic OPAM setup
 ENV NJOBS="2" \
@@ -37,8 +37,9 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages.
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \
-    CI_OPAM="menhir.20190626 elpi.1.4.0 ocamlgraph.1.8.8"
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.10.0 ounit.2.0.8 odoc.1.4.0" \
+    CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
+    BASE_ONLY_OPAM="elpi.1.4.0"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5"
@@ -48,16 +49,16 @@ ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5"
 
 # base switch
 RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
-    opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM
+    opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM $BASE_ONLY_OPAM
 
 # base+32bit switch
 RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
     opam install $BASE_OPAM
 
 # EDGE switch
-ENV COMPILER_EDGE="4.07.1" \
-    COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" \
-    BASE_OPAM_EDGE="dune-release.1.1.0"
+ENV COMPILER_EDGE="4.08.0" \
+    COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta6" \
+    BASE_OPAM_EDGE="dune-release.1.3.1"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index cf95941de5..c7f36ee964 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -3,5 +3,5 @@
 ; Add custom flags here. Default developer profile is `dev`
 (context (opam (switch 4.05.0)))
 (context (opam (switch 4.05.0+32bit)))
-(context (opam (switch 4.07.1)))
-(context (opam (switch 4.07.1+flambda)))
+(context (opam (switch 4.08.0)))
+(context (opam (switch 4.08.0+flambda)))
diff --git a/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst b/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst
new file mode 100644
index 0000000000..8bfd01d7a0
--- /dev/null
+++ b/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst
@@ -0,0 +1,5 @@
+- Coq now officially supports OCaml 4.08.
+
+  see INSTALL files for details
+  (`#10471 <https://github.com/coq/coq/pull/10471>`_,
+  by Emilio Jesús Gallego Arias).
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 2354d2c5e8..7c06bb59f1 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -41,7 +41,7 @@ let _ = CErrors.register_handler begin function
   | Timeout -> CErrors.user_err ~hdr:"Some timeout function" (Pp.str"Timeout!")
   | Exception e -> CErrors.print e
   | TacticFailure e -> CErrors.print e
-  | _ -> Pervasives.raise CErrors.Unhandled
+  | _ -> raise CErrors.Unhandled
 end
 
 (** {6 Non-logical layer} *)
@@ -70,11 +70,11 @@ struct
     let map f a = (); fun () -> f (a ())
   end)
 
-  type 'a ref = 'a Pervasives.ref
+  type 'a ref = 'a Util.pervasives_ref
 
   let ignore a = (); fun () -> ignore (a ())
 
-  let ref a = (); fun () -> Pervasives.ref a
+  let ref a = (); fun () -> ref a
 
   (** [Pervasives.(:=)] *)
   let (:=) r a = (); fun () -> r := a
@@ -93,7 +93,7 @@ struct
         let (src, info) = CErrors.push src in
         h (e, info) ()
 
-  let read_line = fun () -> try Pervasives.read_line () with e ->
+  let read_line = fun () -> try read_line () with e ->
     let (e, info) = CErrors.push e in raise ~info e ()
 
   let print_char = fun c -> (); fun () -> print_char c
diff --git a/engine/proofview.ml b/engine/proofview.ml
index c4a624e462..8b5bd4cd80 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -542,7 +542,7 @@ let tclDISPATCHGEN join tacs =
   let tacs = CList.map branch tacs in
   InfoL.tag (Info.Dispatch) (tclDISPATCHGEN0 join tacs)
 
-let tclDISPATCH tacs = tclDISPATCHGEN Pervasives.ignore tacs
+let tclDISPATCH tacs = tclDISPATCHGEN ignore tacs
 
 let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs
 
@@ -910,7 +910,7 @@ let tclPROGRESS t =
 exception Timeout
 let _ = CErrors.register_handler begin function
   | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
-  | _ -> Pervasives.raise CErrors.Unhandled
+  | _ -> raise CErrors.Unhandled
 end
 
 let tclTIMEOUT n t =
diff --git a/ide/protocol/richpp.ml b/ide/protocol/richpp.ml
index 507b985d2f..463d93af0d 100644
--- a/ide/protocol/richpp.ml
+++ b/ide/protocol/richpp.ml
@@ -94,7 +94,7 @@ let rich_pp width ppcmds =
     print_close_tag = ignore;
   } in
 
-  pp_set_formatter_tag_functions ft tag_functions;
+  pp_set_formatter_tag_functions ft tag_functions [@warning "-3"];
   pp_set_mark_tags ft true;
 
   (* Setting the formatter *)
@@ -107,9 +107,9 @@ let rich_pp width ppcmds =
   (* The whole output must be a valid document. To that
      end, we nest the document inside <pp> tags. *)
   pp_open_box ft 0;
-  pp_open_tag ft "pp";
+  pp_open_tag ft "pp" [@warning "-3"];
   Pp.(pp_with ft ppcmds);
-  pp_close_tag ft ();
+  pp_close_tag ft () [@warning "-3"];
   pp_close_box ft ();
 
   (* Get the resulting XML tree. *)
diff --git a/ide/session.ml b/ide/session.ml
index 3792730455..a9c106a765 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -275,9 +275,9 @@ let make_table_widget ?sort cd cb =
   let make_sorting i (_, c) =
     let sort (store : GTree.model) it1 it2 = match c with
     | `IntC c ->
-      Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c)
+      compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c)
     | `StringC c ->
-      Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c)
+      compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c)
     in
     store#set_sort_func i sort
   in
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index 7758d89ed8..98390e810f 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -15,7 +15,7 @@ struct
     (* we use first size, then usual comparison *)
     let d = String.length s1 - String.length s2 in
     if d <> 0 then d
-    else Pervasives.compare s1 s2
+    else compare s1 s2
 end
 
 module Proposals = Set.Make(StringOrd)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8573dccdf9..e32ef3fe38 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -69,7 +69,7 @@ let print_no_symbol = ref false
 (* Turning notations and scopes on and off for printing *)
 module IRuleSet = Set.Make(struct
     type t = interp_rule
-    let compare x y = Pervasives.compare x y
+    let compare x y = compare x y
   end)
 
 let inactive_notations_table =
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index dc6a1ae180..0ec8b1e0c8 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -12,13 +12,13 @@ open Util
 
 (* Dump of globalization (to be used by coqdoc) *)
 
-let glob_file = ref Pervasives.stdout
+let glob_file = ref stdout
 
 let open_glob_file f =
-  glob_file := Pervasives.open_out f
+  glob_file := open_out f
 
 let close_glob_file () =
-  Pervasives.close_out !glob_file
+  close_out !glob_file
 
 type glob_output_t =
     | NoGlob
@@ -37,7 +37,7 @@ let dump_to_dotglob () = glob_output := MultFiles
 
 let dump_into_file f =
   if String.equal f "stdout" then
-    (glob_output := StdOut; glob_file := Pervasives.stdout)
+    (glob_output := StdOut; glob_file := stdout)
   else
     (glob_output := File f; open_glob_file f)
 
@@ -45,7 +45,7 @@ let feedback_glob () = glob_output := Feedback
 
 let dump_string s =
   if dump () && !glob_output != Feedback then 
-    Pervasives.output_string !glob_file s
+    output_string !glob_file s
 
 let start_dump_glob ~vfile ~vofile =
   match !glob_output with
diff --git a/interp/notation.ml b/interp/notation.ml
index d58125e29b..ec3fad7f7d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -57,7 +57,7 @@ let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLev
 module NotationOrd =
   struct
     type t = notation
-    let compare = Pervasives.compare
+    let compare = pervasives_compare
   end
 
 module NotationSet = Set.Make(NotationOrd)
@@ -593,7 +593,7 @@ let rec rawnum_compare s s' =
    try
      for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done;
      for i = d to l-1 do
-       let c = Pervasives.compare s.[i] s'.[i-d] in
+       let c = pervasives_compare s.[i] s'.[i-d] in
        if c != 0 then raise (Comp c)
      done;
      0
@@ -1242,7 +1242,7 @@ type entry_coercion = notation list
 module EntryCoercionOrd =
  struct
   type t = notation_entry * notation_entry
-   let compare = Pervasives.compare
+   let compare = pervasives_compare
  end
 
 module EntryCoercionMap = Map.Make(EntryCoercionOrd)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index a6b5fc9a41..1a5455cf3a 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -145,7 +145,7 @@ let dummy_symb = SymbValue (dummy_value ())
 
 let eq_symbol sy1 sy2 =
   match sy1, sy2 with
-  | SymbValue v1, SymbValue v2 -> Pervasives.(=) v1 v2 (** FIXME: how is this even valid? *)
+  | SymbValue v1, SymbValue v2 -> (=) v1 v2 (** FIXME: how is this even valid? *)
   | SymbSort s1, SymbSort s2 -> Sorts.equal s1 s2
   | SymbName n1, SymbName n2 -> Name.equal n1 n2
   | SymbConst kn1, SymbConst kn2 -> Constant.equal kn1 kn2
diff --git a/lib/future.ml b/lib/future.ml
index f6e9cee140..01fb7d0297 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -68,7 +68,7 @@ and 'a computation = 'a comput ref
 let unnamed = "unnamed"
 
 let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x =
-  ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x)))
+  ref (Ongoing (name, CEphemeron.create (uuid, f, ref x)))
 let get x =
   match !x with
   | Finished v -> unnamed, UUID.invalid, id, ref (Val v)
diff --git a/lib/pp.ml b/lib/pp.ml
index 542e5f6ecd..2f780677d9 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -197,9 +197,9 @@ let pp_with ft pp =
     | Ppcmd_print_break(m,n)  -> pp_print_break ft m n
     | Ppcmd_force_newline     -> pp_force_newline ft ()
     | Ppcmd_comment coms      -> List.iter (pr_com ft) coms
-    | Ppcmd_tag(tag, s)       -> pp_open_tag  ft tag;
+    | Ppcmd_tag(tag, s)       -> pp_open_tag  ft tag [@warning "-3"];
                                  pp_cmd s;
-                                 pp_close_tag ft ()
+                                 pp_close_tag ft () [@warning "-3"]
   in
   try pp_cmd pp
   with reraise ->
diff --git a/lib/util.ml b/lib/util.ml
index bac06b5701..61678f7669 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -8,6 +8,13 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+type 'a pervasives_ref = 'a ref
+let pervasives_ref = ref
+let pervasives_compare = compare
+let (!) = (!)
+let (+) = (+)
+let (-) = (-)
+
 (* Mapping under pairs *)
 
 let on_fst f (a,b) = (f a,b)
diff --git a/lib/util.mli b/lib/util.mli
index 8ccb4b3f08..b6347126e0 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -8,6 +8,13 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+type 'a pervasives_ref = 'a ref
+val pervasives_ref : 'a -> 'a ref
+val pervasives_compare : 'a -> 'a -> int
+val (!) : 'a ref -> 'a
+val (+) : int -> int -> int
+val (-) : int -> int -> int
+
 (** This module contains numerous utility functions on strings, lists,
    arrays, etc. *)
 
diff --git a/library/summary.ml b/library/summary.ml
index b3ec4c2db2..d3ae42694a 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -153,7 +153,7 @@ let (!) r =
     CEphemeron.get (fst !r)
 
 let ref ?(freeze=fun x -> x) ~name init =
-  let r = Pervasives.ref (CEphemeron.create init, name) in
+  let r = pervasives_ref (CEphemeron.create init, name) in
   declare_summary name
     { freeze_function = (fun ~marshallable -> freeze !r);
       unfreeze_function = ((:=) r);
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9abf212443..109125702c 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -125,7 +125,7 @@ module KOrd =
 struct
   type t = kind * string
   let compare (k1, s1) (k2, s2) =
-    let c = Pervasives.compare k1 k2 (* OK *) in
+    let c = pervasives_compare k1 k2 (* OK *) in
     if c = 0 then String.compare s1 s2
     else c
 end
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 243e0e945c..9d46bbc74e 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -376,7 +376,7 @@ let get_local_profiling_results () = List.hd Local.(!stack)
    own. *)
 module DData = struct
     type t = Feedback.doc_id * Stateid.t
-    let compare x y = Pervasives.compare x y
+    let compare x y = compare x y
 end
 
 module SM = Map.Make(DData)
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 9e735e0680..539536911c 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -156,7 +156,7 @@ let rec prompt level =
   begin
     let open Proofview.NonLogical in
     Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
-    if Pervasives.(!batch) then return (DebugOn (level+1)) else
+    if Util.(!batch) then return (DebugOn (level+1)) else
     let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
     Proofview.NonLogical.catch Proofview.NonLogical.read_line
       begin function (e, info) -> match e with
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 2e32b00c25..24039c93c6 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -93,7 +93,7 @@ let dev_form n_spec  p =
 
 let rec fixpoint f x =
   let y' = f x in
-  if Pervasives.(=) y' x then y'
+  if (=) y' x then y'
   else fixpoint f y'
 
 let  rec_simpl_cone n_spec e = 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index f0435126aa..5cc2c2e061 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1585,7 +1585,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
   let is_proof_compatible (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) =
     let hyps_idx = prover.hyps prf in
     let hyps = selecti hyps_idx old_cl in
-      is_sublist Pervasives.(=) hyps new_cl in
+      is_sublist (=) hyps new_cl in
 
 
 
@@ -1953,7 +1953,7 @@ open Persistent_cache
 
 module Cache = PHashtable(struct
   type t = (provername * micromega_polys)
-  let equal = Pervasives.(=)
+  let equal = (=)
   let hash  = Hashtbl.hash
 end)
 
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index d8f71cda0c..cf5f60fb55 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -136,7 +136,7 @@ let pure_sos  l =
     I should nonetheless be able to try something - over Z  > is equivalent to -1  >= *)
  try
   let l = List.combine l (CList.interval 0 (List.length l -1)) in
-  let (lt,i) =  try (List.find (fun (x,_) -> Pervasives.(=) (snd x) Mc.Strict) l)
+  let (lt,i) =  try (List.find (fun (x,_) -> (=) (snd x) Mc.Strict) l)
    with Not_found -> List.hd l in
   let plt = poly_neg (poly_of_term (expr_to_term (fst lt))) in
   let (n,polys) = sumofsquares plt in (* n * (ci * pi^2) *)
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index 34fb32c270..943bcb384b 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -15,7 +15,7 @@ open Vect
 
 let debug = false
 
-let compare_float (p : float) q = Pervasives.compare p q
+let compare_float (p : float) q = pervasives_compare p q
 
 (** Implementation of intervals *)
 open Itv
@@ -587,7 +587,7 @@ struct
   let optimise vect l =
     (* We add a dummy (fresh) variable for vector *)
     let fresh =
-      List.fold_left (fun fr c -> Pervasives.max fr (Vect.fresh c.coeffs)) 0 l in
+      List.fold_left (fun fr c -> max fr (Vect.fresh c.coeffs)) 0 l in
     let cstr = {
       coeffs = Vect.set fresh (Int (-1)) vect ;
       op = Eq ;
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 97cf23ac1f..537b6175b4 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -21,7 +21,7 @@
 
 module Int = struct
   type t = int
-  let compare : int -> int -> int = Pervasives.compare
+  let compare : int -> int -> int = compare
   let equal  : int -> int -> bool = (=)
 end
 
@@ -354,7 +354,7 @@ struct
 
   let from i = i
   let next i = i + 1
-  let max : int -> int -> int = Pervasives.max
+  let max : int -> int -> int = max
   let pp o i = output_string o (string_of_int i)
   let compare : int -> int -> int = Int.compare
   let to_int x = x
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index f909b4ecda..1a31a36732 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -278,7 +278,7 @@ and op = |Eq | Ge | Gt
 
 exception Strict
 
-let is_strict c = Pervasives.(=) c.op  Gt
+let is_strict c = (=) c.op  Gt
 
 let eval_op = function
   | Eq -> (=/)
@@ -422,7 +422,7 @@ module LinPoly = struct
   let min_list (l:int list) =
     match l with
     | [] -> None
-    | e::l -> Some (List.fold_left Pervasives.min e l)
+    | e::l -> Some (List.fold_left min e l)
 
   let search_linear p l =
     min_list (search_all_linear p l)
@@ -656,9 +656,9 @@ module ProofFormat =  struct
       let rec compare p1 p2 =
         match p1, p2 with
         | Annot(s1,p1) , Annot(s2,p2) -> if s1 = s2 then compare p1 p2
-                                         else Pervasives.compare s1 s2
-        | Hyp i       , Hyp j        -> Pervasives.compare i j
-        | Def i       , Def j        -> Pervasives.compare i j
+                                         else Util.pervasives_compare s1 s2
+        | Hyp i       , Hyp j        -> Util.pervasives_compare i j
+        | Def i       , Def j        -> Util.pervasives_compare i j
         | Cst n       , Cst m        -> Num.compare_num n m
         | Zero        , Zero         -> 0
         | Square v1   , Square v2    -> Vect.compare v1 v2
@@ -667,7 +667,7 @@ module ProofFormat =  struct
         | MulPrf(p1,q1) , MulPrf(p2,q2) -> cmp_pair compare compare (p1,q1) (p2,q2)
         | AddPrf(p1,q1) , MulPrf(p2,q2) -> cmp_pair compare compare (p1,q1) (p2,q2)
         | CutPrf p      , CutPrf p'     -> compare p p'
-        |   _          ,   _            -> Pervasives.compare (id_of_constr p1) (id_of_constr p2)
+        |   _          ,   _            -> Util.pervasives_compare (id_of_constr p1) (id_of_constr p2)
 
     end
 
@@ -785,7 +785,7 @@ module ProofFormat =  struct
       let rec xid_of_hyp i l' =
         match l' with
         | [] -> failwith (Printf.sprintf "id_of_hyp %i %s" hyp (string_of_int_list l))
-        | hyp'::l' -> if Pervasives.(=) hyp hyp' then i else xid_of_hyp (i+1) l' in
+        | hyp'::l' -> if (=) hyp hyp' then i else xid_of_hyp (i+1) l' in
       xid_of_hyp 0 l
 
   end
@@ -873,7 +873,7 @@ module ProofFormat =  struct
        let (p,o) = eval_prf_rule (fun i -> IMap.find i env) prf in
        if is_unsat (p,o) then true
        else
-         if Pervasives.(=) rst Done
+         if (=) rst Done
          then
            begin
              Printf.fprintf stdout "Last inference %a %s\n" LinPoly.pp p (string_of_op o);
diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml
index 15fb55c007..4c95e6da75 100644
--- a/plugins/micromega/simplex.ml
+++ b/plugins/micromega/simplex.ml
@@ -587,7 +587,7 @@ let cut env rmin sol vm (rst:Restricted.t)  tbl (x,v) =
              Printf.printf "This is a cutting plane for %a:" LinPoly.pp_var x;
              Printf.printf " %a\n"  WithProof.output (v,prf);
            end;
-         if Pervasives.(=) (snd v) Eq
+         if (=) (snd v) Eq
          then (* Unsat *) Some (x,(v,prf))
          else
            let vl = (Vect.dotproduct (fst v) (Vect.set 0 (Int 1) sol)) in
@@ -651,7 +651,7 @@ let integer_solver lp =
        match find_cut (!nb mod 2) env cr (*x*) sol vm rst tbl with
        | None -> None
        | Some(cr,((v,op),cut)) ->
-          if Pervasives.(=) op Eq
+          if (=) op Eq
           then (* This is a contradiction *)
             Some(Step(vr,CutPrf cut, Done))
           else
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index e3a9f6f60f..58d5d7ecf1 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -13,7 +13,7 @@ open Num
 (* Comparisons that are reflexive on NaN and also short-circuiting.          *)
 (* ------------------------------------------------------------------------- *)
 
-let cmp = Pervasives.compare (** FIXME *)
+let cmp = compare (** FIXME *)
 
 let (=?) = fun x y -> cmp x y = 0;;
 let (<?) = fun x y -> cmp x y < 0;;
@@ -491,21 +491,21 @@ let temp_path = Filename.get_temp_dir_name ();;
 (* ------------------------------------------------------------------------- *)
 
 let strings_of_file filename =
-  let fd = try Pervasives.open_in filename
+  let fd = try open_in filename
            with Sys_error _ ->
              failwith("strings_of_file: can't open "^filename) in
   let rec suck_lines acc =
-    try let l = Pervasives.input_line fd in
+    try let l = input_line fd in
         suck_lines (l::acc)
     with End_of_file -> List.rev acc in
   let data = suck_lines [] in
-  (Pervasives.close_in fd; data);;
+  (close_in fd; data);;
 
 let string_of_file filename =
   String.concat "\n" (strings_of_file filename);;
 
 let file_of_string filename s =
-  let fd = Pervasives.open_out filename in
+  let fd = open_out filename in
   output_string fd s; close_out fd;;
 
 
diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml
index 4b2bc66eb7..a5f3b83c48 100644
--- a/plugins/micromega/vect.ml
+++ b/plugins/micromega/vect.ml
@@ -148,7 +148,7 @@ let rec add (ve1:t) (ve2:t)  =
   match ve1 , ve2 with
   | [] , v | v , [] -> v
   | (v1,c1)::l1 , (v2,c2)::l2 ->
-     let cmp = Pervasives.compare v1 v2 in
+     let cmp = Util.pervasives_compare v1 v2 in
      if cmp == 0 then
        let s = add_num c1 c2 in
        if eq_num (Int 0) s
@@ -163,7 +163,7 @@ let rec xmul_add (n1:num) (ve1:t) (n2:num) (ve2:t) =
   | [] , _ -> mul n2 ve2
   | _ , [] -> mul n1 ve1
   | (v1,c1)::l1 , (v2,c2)::l2 ->
-     let cmp = Pervasives.compare v1 v2 in
+     let cmp = Util.pervasives_compare v1 v2 in
      if cmp == 0 then
        let s = ( n1 */ c1) +/ (n2 */ c2) in
        if eq_num (Int 0) s
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 6aec83318c..776bd0a829 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -500,7 +500,7 @@ let context sigma operation path (t : constr) =
       | (p, Fix ((_,n as ln),(tys,lna,v))) ->
 	  let l = Array.length v in
 	  let v' = Array.copy v in
-          v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v')))
+          v'.(n)<- loop (Util.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v')))
       | ((P_TYPE :: p), Prod (n,t,c)) ->
           (mkProd (n,loop i p t,c))
       | ((P_TYPE :: p), Lambda (n,t,c)) ->
@@ -684,7 +684,7 @@ let simpl_coeffs path_init path_k =
           | _ -> assert false)
       | _ -> assert false
   in
-  let n = Pervasives.(-) (List.length path_k) (List.length path_init) in
+  let n = Util.(-) (List.length path_k) (List.length path_init) in
   let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl)
   in
   convert_concl ~check:false newc DEFAULTcast
@@ -1000,7 +1000,7 @@ let shrink_pair p f1 f2 =
     | t1,t2 ->
 	begin
 	  oprint t1; print_newline (); oprint t2; print_newline ();
-	  flush Pervasives.stdout; CErrors.user_err Pp.(str "shrink.1")
+          flush stdout; CErrors.user_err Pp.(str "shrink.1")
 	end
 
 let reduce_factor p = function
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index cec87221f0..05c31062fc 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -242,7 +242,7 @@ let add_event, history, clear_history =
   (fun () -> !accu),
   (fun () -> accu := [])
 
-let nf_linear = List.sort (fun x y -> Pervasives.(-) y.v x.v)
+let nf_linear = List.sort (fun x y -> Util.(-) y.v x.v)
 
 let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x))
 
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 34f13b1096..f91b5e7aa2 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -26,7 +26,7 @@ module AdaptorDb = struct
 
   module AdaptorKind = struct
     type t = kind
-    let compare = Pervasives.compare
+    let compare = pervasives_compare
   end
   module AdaptorMap = Map.Make(AdaptorKind)
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index afb546b2d2..496a02f07d 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -58,7 +58,7 @@ let cl_typ_ord t1 t2 = match t1, t2 with
   | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
   | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2
   | CL_IND i1, CL_IND i2 -> ind_ord i1 i2
-  | _ -> Pervasives.compare t1 t2 (** OK *)
+  | _ -> pervasives_compare t1 t2 (** OK *)
 
 module ClTyp = struct
   type t = cl_typ
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 9b1acddef1..64fddd04a3 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -114,7 +114,7 @@ let print_impargs_by_name max = function
 let print_one_impargs_list l =
   let imps = List.filter is_status_implicit l in
   let maximps = List.filter Impargs.maximal_insertion_of imps in
-  let nonmaximps = List.subtract Pervasives.(=) imps maximps in (* FIXME *)
+  let nonmaximps = List.subtract (=) imps maximps in (* FIXME *)
   print_impargs_by_name false nonmaximps @
   print_impargs_by_name true maximps
 
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index a476381b17..70819e9550 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -29,7 +29,7 @@ type term_label =
 
 let compare_term_label t1 t2 = match t1, t2 with
 | GRLabel gr1, GRLabel gr2 -> GlobRef.Ordered.compare gr1 gr2
-| _ -> Pervasives.compare t1 t2 (** OK *)
+| _ -> pervasives_compare t1 t2 (** OK *)
 
 type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 303ddacb67..849ea7e83f 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -257,7 +257,7 @@ let clenv_of_prods poly nprods (c, clenv) gl =
     let sigma = Tacmach.New.project gl in
     let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
     let diff = nb_prod sigma ty - nprods in
-    if Pervasives.(>=) diff 0 then
+    if (>=) diff 0 then
       (* Was Some clenv... *)
       Some (Some diff,
             mk_clenv_from_n gl (Some diff) (c,ty))
diff --git a/tactics/redops.ml b/tactics/redops.ml
index e0473cbefd..86ed8f8899 100644
--- a/tactics/redops.ml
+++ b/tactics/redops.ml
@@ -10,7 +10,7 @@
 
 open Genredexpr
 
-let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *)
+let union_consts l1 l2 = Util.List.union (=) l1 l2 (* FIXME *)
 
 let make_red_flag l =
   let rec add_flag red = function
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 7a07e815ce..6f81be475b 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -297,7 +297,7 @@ module DAG = DAG(struct type t = string let compare = compare end)
 (** TODO: we should share this code with Coqdep_common *)
 module VData = struct
   type t = string list option * string list
-  let compare = Pervasives.compare
+  let compare = Util.pervasives_compare
 end
 
 module VCache = Set.Make(VData)
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index d98242ef17..8beb314046 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -357,7 +357,7 @@ let canonize f =
 
 module VData = struct
   type t = string list option * string list
-  let compare = Pervasives.compare
+  let compare = compare
 end
 
 module VCache = Set.Make(VData)
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 "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n";
@@ -548,13 +548,13 @@ module Html = struct
 
   let trailer () =
     if !header_trailer && !footer_file_spec then
-	let cin = Pervasives.open_in !footer_file in
+        let cin = open_in !footer_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
         if !index && (get_module false) <> "Index" then
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
index bd19d30409..41a4e2a86a 100644
--- a/tools/ocamllibdep.mll
+++ b/tools/ocamllibdep.mll
@@ -35,7 +35,6 @@ rule mllib_list = parse
 
 {
 open Printf
-open Unix
 
 (* Makefile's escaping rules are awful: $ is escaped by doubling and
    other special characters are escaped by backslash prefixing while
@@ -99,6 +98,7 @@ let file_name s = function
 type dir = string option
 
 let add_directory add_file phys_dir =
+  let open Unix in
   Array.iter (fun f ->
     (* we avoid all files starting by '.' *)
     if f.[0] <> '.' then
@@ -152,7 +152,7 @@ let add_caml_known phys_dir f =
     | _ -> ()
 
 let add_caml_dir phys_dir =
-  handle_unix_error (add_directory add_caml_known) phys_dir
+  Unix.handle_unix_error (add_directory add_caml_known) phys_dir
 
 let traite_fichier_modules md ext =
   try
@@ -192,7 +192,7 @@ let mllib_dependencies () =
          efullname efullname;
        printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n"
          efullname efullname;
-       flush Pervasives.stdout)
+       flush stdout)
     (List.rev !mllibAccu)
 
 let mlpack_dependencies () =
@@ -209,7 +209,7 @@ let mlpack_dependencies () =
          efullname efullname;
        printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n"
          efullname efullname;
-       flush Pervasives.stdout)
+       flush stdout)
     (List.rev !mlpackAccu)
 
 let rec parse = function
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index f6211102e6..e49b1c0c07 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -315,8 +315,8 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
 (* Flush in a compatible order with 8.5 *)
 (* This mimics the semantics of the old Pp.flush_all *)
 let loop_flush_all () =
-  Pervasives.flush stderr;
-  Pervasives.flush stdout;
+  flush stderr;
+  flush stdout;
   Format.pp_print_flush !Topfmt.std_ft ();
   Format.pp_print_flush !Topfmt.err_ft ()
 
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