From 24239c17d0b23726ba4005a1f56c56979b2ca2d1 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 25 Feb 2019 10:54:05 +0100
Subject: [PATCH] [ocaml] fix issues following review
---
src/kernel_services/abstract_interp/offsetmap.ml | 2 +-
src/kernel_services/plugin_entry_points/plugin.ml | 3 +--
src/libraries/stdlib/transitioning.ml.in | 9 ++++++---
src/libraries/stdlib/transitioning.mli | 7 +++++++
src/libraries/utils/pretty_utils.ml | 5 +----
5 files changed, 16 insertions(+), 10 deletions(-)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index d605d48d9cc..82625312c80 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -309,7 +309,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
then begin
if current_counter = max_int
then Kernel.fatal "Offsetmap(%s): internal maximum exeeded" V.name;
- counter := pervasives_succ current_counter;
+ counter := Transitioning.Stdlib.succ current_counter;
end;
hashed_node
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index a5c3a0f2f72..bd956deba6c 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -608,7 +608,6 @@ struct
let debug_optname = output_mode "Debug" "debug"
module Debug = struct
- let pervasives_incr = incr (* before 'incr' is shadowed by the one in Int *)
include
Int(struct
let default = !debug_level ()
@@ -629,7 +628,7 @@ struct
(* the level of verbose is at least the level of debug *)
if n > Verbose.get () then Verbose.set n;
if n = 0 then decr positive_debug_ref
- else if old = 0 then pervasives_incr positive_debug_ref);
+ else if old = 0 then Transitioning.Stdlib.incr positive_debug_ref);
if is_kernel () then begin
Cmdline.kernel_debug_atleast_ref := (fun n -> get () >= n);
match !Cmdline.Kernel_debug_level.value_if_set with
diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in
index 2d0204a6532..f96a0faf050 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -57,10 +57,13 @@ let _: ('a -> bool) -> 'a list -> 'a option = find_opt
let _: 'a -> ('a * 'b) list -> 'b option = assoc_opt
let _: 'a -> ('a * 'b) list -> 'b option = assq_opt
-let stdlib_compare = compare (* Pervasives/Stdlib compare *)
-
module Stdlib = struct
- let compare = stdlib_compare
+ (* Pervasives/Stdlib functions *)
+ let compare = compare
+ let succ = succ
+ let incr = incr
+ let min = min
+ let max = max
end
[@@@ warning "-3"]
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index 55a64b4d91b..2da86f65736 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -65,14 +65,21 @@ module List: sig
val assq_opt: 'a -> ('a * 'b) list -> 'b option (** 4.05 *)
end
+(** 4.08 *)
module Stdlib: sig
val compare: 'a -> 'a -> int
+ val succ: int -> int
+ val incr: int ref -> unit
+ val min: 'a -> 'a -> 'a
+ val max: 'a -> 'a -> 'a
end
+(** 4.08 *)
module Dynlink: sig
val init: unit -> unit
end
+(** 4.08 *)
module Format: sig
type stag
val string_of_stag: stag -> string
diff --git a/src/libraries/utils/pretty_utils.ml b/src/libraries/utils/pretty_utils.ml
index f78f4da7009..dc501dd587b 100644
--- a/src/libraries/utils/pretty_utils.ml
+++ b/src/libraries/utils/pretty_utils.ml
@@ -180,14 +180,11 @@ let pp_trail pp fmt x =
(* --- Margins --- *)
(* -------------------------------------------------------------------------- *)
-let pervasives_min = min
-let pervasives_max = max
-
type marger = int ref
let marger () = ref 0
let add_margin marger ?(margin=0) ?(min=0) ?(max=80) text =
let size = String.length text + margin in
- let n = pervasives_min max (pervasives_max min size) in
+ let n = Transitioning.Stdlib.min max (Transitioning.Stdlib.max min size) in
if n > !marger then marger := n
type align = [ `Center | `Left | `Right ]
--
GitLab