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.
---
 plugins/micromega/polynomial.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'plugins/micromega/polynomial.ml')

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);
-- 
cgit v1.2.3