[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.

9 files changed, 25 insertions, 25 deletions

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