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.
---
 engine/logic_monad.ml | 8 ++++----
 engine/proofview.ml   | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'engine')

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