diff --git a/devel_tools/ocamldep_transitive_closure.ml b/devel_tools/ocamldep_transitive_closure.ml
index 3e3290c2246a174c62821a701e6b2c25d5b6fa79..c14aace6a12959ce4b475e66999282221541bd9d 100644
--- a/devel_tools/ocamldep_transitive_closure.ml
+++ b/devel_tools/ocamldep_transitive_closure.ml
@@ -7,7 +7,7 @@ let root = ref ""
module Dep_graph = Graph.Imperative.Digraph.Concrete(
struct
type t = string
- let compare = Pervasives.compare
+ let compare = Transitioning.Stdlib.compare
let hash = Hashtbl.hash
let equal = (=)
end)
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index ef9497abebbceba829913c2c4cf56847fd4b08ca..61d3b38decb7b848f2810cfc9d23433148f28fe0 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -344,7 +344,7 @@ let () =
((Arg.align
(List.sort
(fun (optname1, _, _) (optname2, _, _) ->
- Pervasives.compare optname1 optname2
+ compare optname1 optname2
) argspec)
) @ ["", Arg.Unit (fun () -> ()), example_msg;])
make_test_suite umsg
@@ -1103,7 +1103,7 @@ module Make_Report(M:sig type t end)=struct
(struct
type t = toplevel_command
let project cmd = (cmd.directory,cmd.file,cmd.n)
- let compare c1 c2 = Pervasives.compare (project c1) (project c2)
+ let compare c1 c2 = compare (project c1) (project c2)
let equal c1 c2 = (project c1)=(project c2)
let hash c = Hashtbl.hash (project c)
end)
diff --git a/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index 3d2f1fdd6bff8e142fb2dcfdea076c3b91522f73..655ce87541875983b1a94f8a057f6633241f54c5 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.ml
+++ b/src/kernel_services/abstract_interp/abstract_interp.ml
@@ -432,7 +432,7 @@ module Bool = struct
type t = Top | True | False | Bottom
let hash (b : t) = Hashtbl.hash b
let equal (b1 : t) (b2 : t) = b1 = b2
- let compare (b1 : t) (b2 : t) = Pervasives.compare b1 b2
+ let compare (b1 : t) (b2 : t) = Transitioning.Stdlib.compare b1 b2
let pretty fmt = function
| Top -> Format.fprintf fmt "Top"
| True -> Format.fprintf fmt "True"
diff --git a/src/kernel_services/abstract_interp/float_interval.ml b/src/kernel_services/abstract_interp/float_interval.ml
index 719eaa98d82b78b55698343539bd1a6351e3cf5b..89c49bcc1665585e90cd3eb29bd1c4fd622e20d0 100644
--- a/src/kernel_services/abstract_interp/float_interval.ml
+++ b/src/kernel_services/abstract_interp/float_interval.ml
@@ -171,7 +171,7 @@ module Make (F: Float_sig.S) = struct
let compare x y =
match x, y with
| FRange.Itv (b1, e1, n1), FRange.Itv (b2, e2, n2) ->
- let c = Pervasives.compare n1 n2 in
+ let c = Transitioning.Stdlib.compare n1 n2 in
if c <> 0 then c else
let r = F.compare b1 b2 in
if r <> 0 then r else F.compare e1 e2
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index ff279b93cf08519395f6ef3652339a5a93912ccf..a33a5047ef460dc233a85e1afa1a0b4ffc6131f5 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -129,7 +129,7 @@ module D =
let n = Exp.compare e1 e2 in
if n = 0 then Extlib.compare_basic fk1 fk2 else n
| Memory_access(lv1, access_kind1), Memory_access(lv2, access_kind2) ->
- let n = Pervasives.compare access_kind1 access_kind2 in
+ let n = Transitioning.Stdlib.compare access_kind1 access_kind2 in
if n = 0 then Lval.compare lv1 lv2 else n
| Index_out_of_bound(e11, e12), Index_out_of_bound(e21, e22) ->
let n = Exp.compare e11 e21 in
@@ -141,11 +141,11 @@ module D =
let n = Extlib.opt_compare Exp.compare e11 e21 in
if n = 0 then Exp.compare e12 e22 else n
| Overflow(s1, e1, n1, b1), Overflow(s2, e2, n2, b2) ->
- let n = Pervasives.compare s1 s2 in
+ let n = Transitioning.Stdlib.compare s1 s2 in
if n = 0 then
let n = Exp.compare e1 e2 in
if n = 0 then
- let n = Pervasives.compare b1 b2 in
+ let n = Transitioning.Stdlib.compare b1 b2 in
if n = 0 then Integer.compare n1 n2 else n
else
n
@@ -154,7 +154,7 @@ module D =
| Float_to_int(e1, n1, b1), Float_to_int(e2, n2, b2) ->
let n = Exp.compare e1 e2 in
if n = 0 then
- let n = Pervasives.compare b1 b2 in
+ let n = Transitioning.Stdlib.compare b1 b2 in
if n = 0 then Integer.compare n1 n2 else n
else
n
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index d61e7eec939bc5495e058724901f21d606f8bf2e..ccba7c4f34b98bd4947c104ab47e58a8c5c390d9 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -562,7 +562,7 @@ include Datatype.Make_with_collections
let n = Extlib.opt_compare Kf.compare kf1 kf2 in
if n = 0 then
let n = Kinstr.compare ki1 ki2 in
- if n = 0 then Pervasives.compare ba1 ba2 else n
+ if n = 0 then Transitioning.Stdlib.compare ba1 ba2 else n
else
n
| IPAxiom (s1,_,_,_,_), IPAxiom (s2,_,_,_,_)
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index 10e25594bfed19cfedf49dca7ae9938475b680cf..4842bcdeb30cff1a9acb5f5cdca88897ed7a8894 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -47,7 +47,7 @@ module Emitted_status =
| True -> "VALID"
| False_if_reachable | False_and_reachable -> "**NOT** VALID"
| Dont_know -> "unknown")
- let compare (s1:t) s2 = Pervasives.compare s1 s2
+ let compare (s1:t) s2 = Transitioning.Stdlib.compare s1 s2
let equal (s1:t) s2 = s1 = s2
let hash (s:t) = Caml_hashtbl.hash s
end)
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index 6544c2ba0cbb5055d14e179024bd7821292d189b..ade7c65cc86b8c94b7cacbb38c36a9cc19367c00 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -409,7 +409,7 @@ type order =
| A of Datatype.String.Set.t
let cmp_order a b = match a , b with
- | I a , I b -> Pervasives.compare a b
+ | I a , I b -> Transitioning.Stdlib.compare a b
| I _ , _ -> (-1)
| _ , I _ -> 1
| S a , S b -> String.compare a b
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index a4d1063fa01f085b1b38233f55f92aa5a1518d05..17b141196aacedcb19746db9f02ac4d65c8a38aa 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -1584,7 +1584,7 @@ and compare_toffset off1 off2 =
and compare_logic_label l1 l2 = match l1, l2 with
| StmtLabel s1 , StmtLabel s2 -> Stmt.compare !s1 !s2
| FormalLabel s1, FormalLabel s2 -> String.compare s1 s2
- | BuiltinLabel l1, BuiltinLabel l2 -> Pervasives.compare l1 l2
+ | BuiltinLabel l1, BuiltinLabel l2 -> Transitioning.Stdlib.compare l1 l2
| (StmtLabel _ | FormalLabel _), (FormalLabel _ | BuiltinLabel _) -> -1
| (BuiltinLabel _ | FormalLabel _), (StmtLabel _ | FormalLabel _) -> 1
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 0632240c7cabaf813a28d995b8a73d938b2bdb40..7621c2488ce42a79de03329e5905cd99326104b1 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -284,7 +284,7 @@ module DatatypeMachdep = Datatype.Make_with_collections(struct
let reprs = [Machdeps.x86_32]
let name = "File.Machdep"
type t = Cil_types.mach
- let compare : t -> t -> int = Pervasives.compare
+ let compare : t -> t -> int = Transitioning.Stdlib.compare
let equal : t -> t -> bool = (=)
let hash : t -> int = Hashtbl.hash
let copy = Datatype.identity
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 918ca0447b734454367bde0b04082b03bec3ff96..3696935c9266797f8316aa6d5b0fedc9d83bedd0 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -457,7 +457,7 @@ module Type_namespace =
let reprs = [Typedef]
let name = "Logic_typing.type_namespace"
type t = type_namespace
- let compare : t -> t -> int = Pervasives.compare
+ let compare : t -> t -> int = Transitioning.Stdlib.compare
let equal : t -> t -> bool = (=)
let hash : t -> int = Hashtbl.hash
end)
@@ -3593,7 +3593,7 @@ struct
struct
type t = string list
let compare s1 s2 =
- Pervasives.(compare (List.sort compare s1) (List.sort compare s2))
+ Transitioning.Stdlib.(compare (List.sort compare s1) (List.sort compare s2))
end)
let type_spec old_behaviors loc is_stmt_contract result env s =
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 9ad4de7713352889d31e310614767229efa173fa..352824e171c1585f0746e879da519a37f82c871a 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1544,12 +1544,12 @@ let rec compare_term t1 t2 =
| TAlignOfE _, _ -> 1
| _, TAlignOfE _ -> -1
| TUnOp (o1,t1), TUnOp(o2,t2) ->
- let res = Pervasives.compare o1 o2 in
+ let res = Transitioning.Stdlib.compare o1 o2 in
if res = 0 then compare_term t1 t2 else res
| TUnOp _, _ -> 1
| _, TUnOp _ -> -1
| TBinOp(o1,l1,r1), TBinOp(o2,l2,r2) ->
- let res = Pervasives.compare o1 o2 in
+ let res = Transitioning.Stdlib.compare o1 o2 in
if res = 0 then
let res = compare_term l1 l2 in
if res = 0 then compare_term r1 r2 else res
@@ -1749,7 +1749,7 @@ and compare_predicate_node p1 p2 =
| Papp _, _ -> 1
| _, Papp _ -> -1
| Prel(r1,lt1,rt1), Prel(r2,lt2,rt2) ->
- let res = Pervasives.compare r1 r2 in
+ let res = Transitioning.Stdlib.compare r1 r2 in
if res = 0 then
let res = compare_term lt1 lt2 in
if res = 0 then compare_term rt1 rt2 else res
diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml
index 9752b11209c61111831cfa57d7b0ce6dfea3e5a9..328b9e1a1e39b56e6dc0ed6d23b889c58749eadc 100644
--- a/src/libraries/datatype/datatype.ml
+++ b/src/libraries/datatype/datatype.ml
@@ -1776,7 +1776,7 @@ module Bool =
let name = "bool"
let reprs = [ true ]
let copy = identity
- let compare : bool -> bool -> int = Pervasives.compare
+ let compare : bool -> bool -> int = Transitioning.Stdlib.compare
let equal : bool -> bool -> bool = (=)
let pretty fmt b = Format.fprintf fmt "%B" b
let varname _ = "b"
@@ -1790,12 +1790,12 @@ module Int = struct
let name = "int"
let reprs = [ 2 ]
let copy = identity
- let compare : int -> int -> int = Pervasives.compare
+ let compare : int -> int -> int = Transitioning.Stdlib.compare
let equal : int -> int -> bool = (=)
let pretty fmt n = Format.fprintf fmt "%d" n
let varname _ = "n"
end)
- let compare : int -> int -> int = Pervasives.compare
+ let compare : int -> int -> int = Transitioning.Stdlib.compare
end
let int = Int.ty
@@ -1848,7 +1848,7 @@ module Float =
let name = "float"
let reprs = [ 0.1 ]
let copy = identity
- let compare : float -> float -> int = Pervasives.compare
+ let compare : float -> float -> int = Transitioning.Stdlib.compare
let equal : float -> float -> bool = (=)
let pretty fmt f = Format.fprintf fmt "%f" f
let varname _ = "f"
diff --git a/src/libraries/stdlib/FCHashtbl.ml b/src/libraries/stdlib/FCHashtbl.ml
index 4e84f1b3ced33540d4cb72ff7b1f797937ef2bfe..a19c31b59965524a171ab964b38ff6c8e7bc7e02 100644
--- a/src/libraries/stdlib/FCHashtbl.ml
+++ b/src/libraries/stdlib/FCHashtbl.ml
@@ -50,7 +50,7 @@ module Make(H: Hashtbl.HashedType) : S with type key = H.t = struct
include Hashtbl.Make(H)
- let fold_sorted ?(cmp=Pervasives.compare) f h acc =
+ let fold_sorted ?(cmp=Transitioning.Stdlib.compare) f h acc =
let module Aux = struct type t = key let compare = cmp end in
let module M = FCMap.Make(Aux) in
let add k v m =
diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in
index 7848ea531cf64c73f651b3c74ca0aa0309f2d736..5dac32656eb7b41f7d6474f6a0d7d9a6a8d5f470 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -57,6 +57,12 @@ 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
+end
+
[@@@ warning "-3"]
module String = struct
diff --git a/src/libraries/utils/bitvector.ml b/src/libraries/utils/bitvector.ml
index a1dfcfa38a4fedeaedb472bed9e4da705168d501..36657b9600b294c8aafb2391f85cc6c3de3e41b9 100644
--- a/src/libraries/utils/bitvector.ml
+++ b/src/libraries/utils/bitvector.ml
@@ -223,7 +223,7 @@ let bitwise_op4 size op4 a b c d =
let equal = (=);; (* String equality. *)
-let compare = Pervasives.compare
+let compare = Transitioning.Stdlib.compare
let hash = Hashtbl.hash
let concat bv1 size1 bv2 size2 =
diff --git a/src/libraries/utils/json.mll b/src/libraries/utils/json.mll
index 8444a4bc8ed32eb86fd517fedf9d7fd74143df47..a2123702f152a5d6611126dae17f60572843f638 100644
--- a/src/libraries/utils/json.mll
+++ b/src/libraries/utils/json.mll
@@ -37,7 +37,7 @@ type json =
type t = json
let equal = (=)
-let compare = Pervasives.compare
+let compare = Transitioning.Stdlib.compare
type token = EOF | TRUE | FALSE | NULL | KEY of char
| STR of string | INT of string | DEC of string
diff --git a/src/libraries/utils/pretty_utils.ml b/src/libraries/utils/pretty_utils.ml
index 3ecc2ed1913e5f0d15842863071b9cd74435c621..f78f4da7009bf433f26aa5c18427c3a6244846ac 100644
--- a/src/libraries/utils/pretty_utils.ml
+++ b/src/libraries/utils/pretty_utils.ml
@@ -48,7 +48,7 @@ let rec pp_print_string_fill out s =
Format.fprintf out "%s@ %a" s1 pp_print_string_fill s2
end else Format.pp_print_string out s
-type sformat = (unit,Format.formatter,unit) Pervasives.format
+type sformat = (unit,Format.formatter,unit) format
type 'a formatter = Format.formatter -> 'a -> unit
type ('a,'b) formatter2 = Format.formatter -> 'a -> 'b -> unit
@@ -180,11 +180,14 @@ 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 = pervasives_min max (pervasives_max min size) in
if n > !marger then marger := n
type align = [ `Center | `Left | `Right ]
diff --git a/src/libraries/utils/pretty_utils.mli b/src/libraries/utils/pretty_utils.mli
index c0cfa39b1b6543cf0fc3e5d46704bb93846ed55b..416e56e9d08e548fc15a276239e0d5ae7fcb8a12 100644
--- a/src/libraries/utils/pretty_utils.mli
+++ b/src/libraries/utils/pretty_utils.mli
@@ -70,7 +70,7 @@ val escape_underscores : string -> string
(** {2 pretty printers for standard types} *)
(* ********************************************************************** *)
-type sformat = (unit,Format.formatter,unit) Pervasives.format
+type sformat = (unit,Format.formatter,unit) format
type 'a formatter = Format.formatter -> 'a -> unit
type ('a,'b) formatter2 = Format.formatter -> 'a -> 'b -> unit
diff --git a/src/libraries/utils/rgmap.ml b/src/libraries/utils/rgmap.ml
index 054bb4b9cfac56c9129dd6daf04d862a9df3feed..d1c4fd78aee633698806adde8331fae90c5311b6 100644
--- a/src/libraries/utils/rgmap.ml
+++ b/src/libraries/utils/rgmap.ml
@@ -42,7 +42,7 @@ type 'a entry = int * int * 'a
module Wmap = Map.Make
(struct
type t = int
- let compare (a:t) (b:t) = Pervasives.compare a b
+ let compare (a:t) (b:t) = Transitioning.Stdlib.compare a b
end)
module Rmap = Map.Make
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index 5a1f810e04f26cce0e71f89a660a2a358325d27e..c17460dafd93064ba107970be47df602c24ab43e 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -164,8 +164,8 @@ struct
if (pe1 = pe2) then 0
else
(* most englobing comes first *)
- Pervasives.compare pe2 pe1
- else Pervasives.compare pb1 pb2
+ Transitioning.Stdlib.compare pe2 pe1
+ else Transitioning.Stdlib.compare pb1 pb2
) arr
;
arr
diff --git a/src/plugins/gui/warning_manager.ml b/src/plugins/gui/warning_manager.ml
index c27f8f1070dd489bb877a35ee0597d8e7755f003..bac5362ceb8b11063002fc26cef28d0e1a55a861 100644
--- a/src/plugins/gui/warning_manager.ml
+++ b/src/plugins/gui/warning_manager.ml
@@ -34,7 +34,7 @@ type t =
module Data = Indexer.Make(
struct
type t = int*row
- let compare (x,_) (y,_) = Pervasives.compare x y
+ let compare (x,_) (y,_) = Transitioning.Stdlib.compare x y
end)
let make ~packing ~callback =
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index 9eb22f91a2d9727170f3ed7feb4acca0819f6c86..f10bf8fd03428dab4164c037d96e01dad29dd005 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -265,7 +265,7 @@ let get_file_type filename =
module VarinfoByName = struct
type t = Cil_types.varinfo
- let compare v1 v2 = Pervasives.compare v1.vname v2.vname
+ let compare v1 v2 = Transitioning.Stdlib.compare v1.vname v2.vname
end
(** Map and sets of varinfos sorted by name (and not by ids) *)
diff --git a/src/plugins/obfuscator/obfuscator_kind.ml b/src/plugins/obfuscator/obfuscator_kind.ml
index 216651aca09b951745e6b6639b3be7cbf2f14f8f..f4f1fb22e5b396056789b6d543d1b17e1283e04a 100644
--- a/src/plugins/obfuscator/obfuscator_kind.ml
+++ b/src/plugins/obfuscator/obfuscator_kind.ml
@@ -69,7 +69,7 @@ include Datatype.Make_with_collections
let reprs = [ Global_var ]
let hash (k:k) = Hashtbl.hash k
let equal (k1:k) k2 = k1 = k2
- let compare (k1:k) k2 = Pervasives.compare k1 k2
+ let compare (k1:k) k2 = Transitioning.Stdlib.compare k1 k2
let varname _ = "k"
let internal_pretty_code = Datatype.undefined
let copy = Datatype.identity
diff --git a/src/plugins/qed/export.ml b/src/plugins/qed/export.ml
index b36fca33b8152f2f7dcba4a777d08de35fdf37f7..8f7d667899f2fa0b28b3496fffc9ecc3457c4b98 100644
--- a/src/plugins/qed/export.ml
+++ b/src/plugins/qed/export.ml
@@ -828,7 +828,7 @@ struct
(fun (s1,e1) (s2,e2) ->
match s1,s2 with
| true,true | false,false ->
- Pervasives.compare (T.weigth e1) (T.weigth e2)
+ Transitioning.Stdlib.compare (T.weigth e1) (T.weigth e2)
| true,false -> (-1)
| false,true -> 1
) sxs in
diff --git a/src/plugins/qed/intmap.ml b/src/plugins/qed/intmap.ml
index 70ded406022bd1b52ee7eedd9236f579e9f76dd3..e6b77689d3a68bf9708da7390cab08c23d11fef4 100644
--- a/src/plugins/qed/intmap.ml
+++ b/src/plugins/qed/intmap.ml
@@ -211,12 +211,12 @@ let rec compare cmp s t =
| Empty , _ -> (-1)
| _ , Empty -> 1
| Lf(i,x) , Lf(j,y) ->
- let ck = Pervasives.compare i j in
+ let ck = Transitioning.Stdlib.compare i j in
if ck = 0 then cmp x y else ck
| Lf _ , _ -> (-1)
| _ , Lf _ -> 1
| Br(p,s0,s1) , Br(q,t0,t1) ->
- let cp = Pervasives.compare p q in
+ let cp = Transitioning.Stdlib.compare p q in
if cp <> 0 then cp else
let c0 = compare cmp s0 t0 in
if c0 <> 0 then c0 else
diff --git a/src/plugins/qed/kind.ml b/src/plugins/qed/kind.ml
index 93d8d7fae87f4b8c513545a64548ea6273696858..e9207939eb1d3e238e6c3dc4810ab93ca36a0c77 100644
--- a/src/plugins/qed/kind.ml
+++ b/src/plugins/qed/kind.ml
@@ -177,7 +177,7 @@ let rec compare_tau cfield cadt t1 t2 =
| Prop , Prop -> 0
| Prop , _ -> (-1)
| _ , Prop -> 1
- | Tvar k , Tvar k' -> Pervasives.compare k k'
+ | Tvar k , Tvar k' -> Transitioning.Stdlib.compare k k'
| Tvar _ , _ -> (-1)
| _ , Tvar _ -> 1
| Array(ta,tb) , Array(ta',tb') ->
diff --git a/src/plugins/qed/pool.ml b/src/plugins/qed/pool.ml
index 868e99b8a5791a5c5ac6e8a43aba25690daf7a51..bdb043a9aadbd75edf4d6c3312fbb346da6263da 100644
--- a/src/plugins/qed/pool.ml
+++ b/src/plugins/qed/pool.ml
@@ -77,9 +77,9 @@ struct
let compare x y =
let cmp = String.compare x.vbase y.vbase in
if cmp <> 0 then cmp else
- let cmp = Pervasives.compare x.vrank y.vrank in
+ let cmp = Transitioning.Stdlib.compare x.vrank y.vrank in
if cmp <> 0 then cmp else
- Pervasives.compare x.vid y.vid
+ Transitioning.Stdlib.compare x.vid y.vid
(* POOL *)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 0c05374f3a184680de0625a57c77d8cbced021aa..fa6e17a4ddec2150f394086d0898031297e621f6 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -379,7 +379,7 @@ struct
| Constructor -> 1
| Operator _ -> 0
- let cmp_size a b = Pervasives.compare a.size b.size
+ let cmp_size a b = Transitioning.Stdlib.compare a.size b.size
let rank_bind = function Forall -> 0 | Exists -> 1 | Lambda -> 2
let cmp_bind p q = rank_bind p - rank_bind q
let cmp_field phi (f,x) (g,y) =
@@ -1221,7 +1221,7 @@ struct
| _ -> (k,t) :: acc
(* sorts monoms by terms *)
- let compare_monoms (_,t1) (_,t2) = Pervasives.compare t1.id t2.id
+ let compare_monoms (_,t1) (_,t2) = Transitioning.Stdlib.compare t1.id t2.id
(* factorized monoms *)
let fold_monom ts k t =
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index f14ae80130e34ff8adf403f3605582636f5ad075..1d3a931ccf0f44484a297421ac1b53e8b7d59f5f 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -242,7 +242,7 @@ let json_of_event e =
module EVENTS = Set.Make
(struct
type t = event
- let compare = Pervasives.compare
+ let compare = Transitioning.Stdlib.compare
end)
let events_queue = Queue.create ()
diff --git a/src/plugins/report/csv.ml b/src/plugins/report/csv.ml
index 643168a388f3184f1ae4eea2a25a6995aa887656..7064555e9a0077894970da26a11b6673232a94fc 100644
--- a/src/plugins/report/csv.ml
+++ b/src/plugins/report/csv.ml
@@ -66,7 +66,7 @@ let lines () =
emitted on statements copied through loop unrolling. This is the desired
semantics for now. However, since we compare entire locations, textually
identical lines that refer to different expressions are kept separate *)
- Extlib.sort_unique Pervasives.compare l
+ Extlib.sort_unique Transitioning.Stdlib.compare l
let output file =
let ch = open_out file in
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index 062f57f05174f880780c1207d6b44d8f42d9f9ec..58e5b96280fd67851df297755143e0bfd2c0bd0e 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -48,7 +48,7 @@ module Status = struct
let reprs = [ True; False; False; Unknown ]
let mem_project = Datatype.never_any_project
let pretty = pretty_status
- let compare (s1:t) (s2:t) = Pervasives.compare s1 s2
+ let compare (s1:t) (s2:t) = Transitioning.Stdlib.compare s1 s2
let equal (s1:t) (s2:t) = s1 = s2
let hash (s:t) = Hashtbl.hash s
end)
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index ce361f8068a847ba4c0735e85ecc16a3cebad1e3..78284d2e1d4a394ff72b29b142cf3d7e439d4830 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -502,7 +502,7 @@ module G = struct
let compare ii1 ii2 = match ii1, ii2 with
| PreciseIteration i1, PreciseIteration i2 ->
- Pervasives.compare i1 i2
+ Transitioning.Stdlib.compare i1 i2
| MultipleIterations i1, MultipleIterations i2 ->
MultipleIterations.compare i1 i2
| PreciseIteration _, MultipleIterations _ -> -1
diff --git a/src/plugins/value/gui_files/gui_callstacks_manager.ml b/src/plugins/value/gui_files/gui_callstacks_manager.ml
index d75eefad24279240861c589c4aa2a7199f74d8a5..18098708557657587fb0f99f93a7702e3e9ca292 100644
--- a/src/plugins/value/gui_files/gui_callstacks_manager.ml
+++ b/src/plugins/value/gui_files/gui_callstacks_manager.ml
@@ -261,7 +261,7 @@ module Make (Input: Input) = struct
module Data = Indexer.Make(
struct
type t = int * value row
- let compare (x,_) (y,_) = Pervasives.compare x y
+ let compare (x,_) (y,_) = Transitioning.Stdlib.compare x y
end)
(* This function creates a single GTree that displays per-callstack
diff --git a/src/plugins/value/gui_files/gui_red.ml b/src/plugins/value/gui_files/gui_red.ml
index 03929af50d5f22280fc3dec000de633004b5d86e..4b807209ea73577e1a3e4bdd3e65cfab925630f6 100644
--- a/src/plugins/value/gui_files/gui_red.ml
+++ b/src/plugins/value/gui_files/gui_red.ml
@@ -108,7 +108,7 @@ type t =
module Data = Indexer.Make(
struct
type t = int*row
- let compare (x,_) (y,_) = Pervasives.compare x y
+ let compare (x,_) (y,_) = Transitioning.Stdlib.compare x y
end)
let append t message = t.append message
diff --git a/src/plugins/value/utils/structure.ml b/src/plugins/value/utils/structure.ml
index af63dc0f92d72a2a76c7fa92211b4802e02d1cc5..30f4b3c38637a85fc888f4e7541ed9cf7b89f51d 100644
--- a/src/plugins/value/utils/structure.ml
+++ b/src/plugins/value/utils/structure.ml
@@ -62,7 +62,7 @@ module Make (X : sig end) = struct
then Some ((Obj.magic (Eq : (a,a) eq)) : (a,b) eq)
else None
- let compare x y = Pervasives.compare x.tag y.tag
+ let compare x y = Transitioning.Stdlib.compare x.tag y.tag
let hash x = x.tag
let tag x = x.tag
diff --git a/src/plugins/value/utils/value_perf.ml b/src/plugins/value/utils/value_perf.ml
index 9476dbbb11f8dd59b13b986fb989f0bb918a95a2..7015fc9e3f38dcadffcadeba2e489920bf3226b2 100644
--- a/src/plugins/value/utils/value_perf.ml
+++ b/src/plugins/value/utils/value_perf.ml
@@ -88,7 +88,7 @@ module Call_info = struct
(* Sorts call_infos by decreasing execution time. *)
let cmp current_time ci1 ci2 =
- - (Pervasives.compare (total_duration current_time ci1) (total_duration current_time ci2))
+ - (Transitioning.Stdlib.compare (total_duration current_time ci1) (total_duration current_time ci2))
;;
(* From an iteration, filter and sort by call_info, and returns the
diff --git a/src/plugins/value/values/numerors/numerors_interval.ml b/src/plugins/value/values/numerors/numerors_interval.ml
index bb9f4c20a7d2b931b41a6d160b0bc5c07bc3191e..114b2fba184e2676e35ae1068c1c032193442e4b 100644
--- a/src/plugins/value/values/numerors/numerors_interval.ml
+++ b/src/plugins/value/values/numerors/numerors_interval.ml
@@ -171,7 +171,7 @@ let compare a b = (a, b) >>+ fun _ ->
match a, b with
| NaN _, NaN _ -> 0 | NaN _, _ -> 1 | _, NaN _ -> -1
| I (x, y, n), I (x', y', n') ->
- let c = Pervasives.compare n n' in
+ let c = Transitioning.Stdlib.compare n n' in
if c = 0 then
let c = F.compare x x' in
if c = 0 then F.compare y y'
diff --git a/src/plugins/value/values/numerors/numerors_utils.ml b/src/plugins/value/values/numerors/numerors_utils.ml
index b456540037a4cf3864cdd94c2955030e80216a6a..dd45d7afeb77a4a803d64a81cd9d25cc61c9c44c 100644
--- a/src/plugins/value/values/numerors/numerors_utils.ml
+++ b/src/plugins/value/values/numerors/numerors_utils.ml
@@ -59,7 +59,7 @@ module Precisions = struct
| Simple -> -149 | Double -> -1074
| Long_Double -> -16494 | Real -> Pervasives.min_int
- let compare a b = Pervasives.compare (get a) (get b)
+ let compare a b = Transitioning.Stdlib.compare (get a) (get b)
let eq a b = compare a b = 0
let max a b = if compare a b <= 0 then b else a
diff --git a/src/plugins/value/values/sign_value.ml b/src/plugins/value/values/sign_value.ml
index 2a6908fcf334bc60a6ace07bf11fbdeeb28be111..211ce3cd5b2891d14d9a44a6e6f5862aed9eb762 100644
--- a/src/plugins/value/values/sign_value.ml
+++ b/src/plugins/value/values/sign_value.ml
@@ -54,7 +54,7 @@ let empty = { pos = false; zero = false; neg = false }
include Datatype.Make(struct
type t = signs
include Datatype.Serializable_undefined
- let compare = Pervasives.compare
+ let compare = Transitioning.Stdlib.compare
let equal = Datatype.from_compare
let hash = Hashtbl.hash
let reprs = [top]
diff --git a/src/plugins/wp/CfgCompiler.ml b/src/plugins/wp/CfgCompiler.ml
index 88e5892d9bd0b61e6faa5341bb51aeaba0c6621a..6109ac2d892a28f893ed5805e24735bdc900c479 100644
--- a/src/plugins/wp/CfgCompiler.ml
+++ b/src/plugins/wp/CfgCompiler.ml
@@ -440,7 +440,7 @@ struct
let pp fmt = function | Node i -> Node.pp fmt i | Assume (i,_) -> Format.fprintf fmt "ass%i" i
| Check (i,_) -> Format.fprintf fmt "chk%i" i
let equal x y = (tag x) = (tag y)
- let compare x y = Pervasives.compare (tag x) (tag y)
+ let compare x y = Transitioning.Stdlib.compare (tag x) (tag y)
let hash x = tag x
end in
let module G = Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (V)(E) in
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 1fac69012b52aeae87e0b8ee5df50b9315ac4c54..3362fc39f4d25f1e4e29eea574d771ba64ce37a0 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -270,7 +270,7 @@ struct
| _ -> 2
in
let r = rank s1.condition - rank s2.condition in
- if r = 0 then Pervasives.compare k2 k1 else r
+ if r = 0 then Transitioning.Stdlib.compare k2 k1 else r
end)
type t = Vars.t * SEQ.t
diff --git a/src/plugins/wp/Cstring.ml b/src/plugins/wp/Cstring.ml
index 66f3ab3afb6e32672107fa09484c648640827026..f678abdd424048e1d6069157c3806b0302707a52 100644
--- a/src/plugins/wp/Cstring.ml
+++ b/src/plugins/wp/Cstring.ml
@@ -35,7 +35,7 @@ type cst =
module STR =
struct
type t = cst
- let compare = Pervasives.compare (* only comparable types *)
+ let compare = Transitioning.Stdlib.compare (* only comparable types *)
let pretty fmt = function
| C_str s -> Format.fprintf fmt "%S" s
| W_str _ -> Format.fprintf fmt "\"L<...>\""
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index bc0f3667d600ba5553a818df622c507c70a01f48..bc76ceb0d8180a2944f420e6fe6386235ca401c4 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -274,7 +274,7 @@ module COMPILERS = FCMap.Make
(struct
type t = setup * driver
let compare (s,d) (s',d') =
- let cmp = Pervasives.compare s s' in
+ let cmp = Transitioning.Stdlib.compare s s' in
if cmp <> 0 then cmp else LogicBuiltins.compare d d'
end)
diff --git a/src/plugins/wp/LogicBuiltins.ml b/src/plugins/wp/LogicBuiltins.ml
index a34105fae018047c8194da662cbf79aa356b8e41..7e0b7b17c2b8a2a4fbe785bf7110f4950f15e443 100644
--- a/src/plugins/wp/LogicBuiltins.ml
+++ b/src/plugins/wp/LogicBuiltins.ml
@@ -43,7 +43,7 @@ type kind =
| F of Ctypes.c_float
| A (* abstract data *)
-(* [LC] kinds can be compared by Pervasives.compare *)
+(* [LC] kinds can be compared by Stdlib.compare *)
let okind = function
| C_int i -> I i
@@ -157,14 +157,14 @@ let iter_table f =
Hashtbl.iter
(fun a sigs -> List.iter (fun (ks,lnk) -> items := (a,ks,lnk)::!items) sigs)
(cdriver ()).hlogic ;
- List.iter f (List.sort Pervasives.compare !items)
+ List.iter f (List.sort Transitioning.Stdlib.compare !items)
let iter_libs f =
let items = ref [] in
Hashtbl.iter
(fun a libs -> items := (a,libs) :: !items)
(cdriver ()).hdeps ;
- List.iter f (List.sort Pervasives.compare !items)
+ List.iter f (List.sort Transitioning.Stdlib.compare !items)
let dump () =
Log.print_on_output
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 410076e90d5b76643c128246e264f40d836807d6..6de0a92ea470f46ac2559dbef0a92a60dd5edc15 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -651,7 +651,7 @@ let shift l obj k = e_fun (Shift.get obj) [l;k]
module LITERAL =
struct
type t = int * Cstring.cst
- let compare (a:t) (b:t) = Pervasives.compare (fst a) (fst b)
+ let compare (a:t) (b:t) = Transitioning.Stdlib.compare (fst a) (fst b)
let pretty fmt (eid,cst) = Format.fprintf fmt "%a@%d" Cstring.pretty cst eid
end
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 3ccf4f59b6873a055a172ced0622f3e5ae6cfbbf..e628fe6a352255bf984f4f6aaa120c148e7226e3 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -47,7 +47,7 @@ struct
let sa = stage a in
let sb = stage b in
if sa = sb
- then Pervasives.compare (time a) (time b)
+ then Transitioning.Stdlib.compare (time a) (time b)
else sa - sb
let sort script = List.stable_sort compare script
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 4480ea68e99f8fb138ab27deed9f3208e2ce5a04..56cbd3f35d0ef00ad13a1781a3a94ceee09e6b34 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -314,7 +314,7 @@ type goal =
module Goal =
struct
type t = goal
- let compare = Pervasives.compare
+ let compare = Transitioning.Stdlib.compare
let pretty fmt g =
Format.fprintf fmt "[%s]%s.%s" g.file g.theory g.goal
end
diff --git a/src/plugins/wp/Splitter.ml b/src/plugins/wp/Splitter.ml
index 9ac78de77206ef6f1c7f1dc2d95e54cb5865706c..c7afbd32731372465883e617ebeaa5026cbac0da 100644
--- a/src/plugins/wp/Splitter.ml
+++ b/src/plugins/wp/Splitter.ml
@@ -68,7 +68,7 @@ let compare p q =
| _ , ELSE _ -> 1
| CASE(s1,k1) , CASE(s2,k2) ->
let c = Stmt.compare s1 s2 in
- if c = 0 then Pervasives.compare k1 k2 else c
+ if c = 0 then Transitioning.Stdlib.compare k1 k2 else c
| CASE _ , _ -> (-1)
| _ , CASE _ -> 1
| DEFAULT s , DEFAULT t -> Stmt.compare s t
@@ -80,7 +80,7 @@ let compare p q =
| CALL _ , _ -> (-1)
| _ , CALL _ -> 1
| ASSERT(ip1,k1,_) , ASSERT(ip2,k2,_) ->
- let c = Pervasives.compare ip1.ip_id ip2.ip_id in
+ let c = Transitioning.Stdlib.compare ip1.ip_id ip2.ip_id in
if c = 0 then k1 - k2 else c
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index 968c460cb2b5941bbe21304fc8ea819281bf9330..1a9c9791b6c6305bf21a1717d8009696620cba8f 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/src/plugins/wp/StmtSemantics.ml
@@ -499,7 +499,7 @@ struct
| NoneInfo, NoneInfo -> 0
| NoneInfo, _ -> -1
| _ , NoneInfo -> 1
- | LoopHead i, LoopHead j -> Pervasives.compare j i
+ | LoopHead i, LoopHead j -> Transitioning.Stdlib.compare j i
module Automata = Interpreted_automata.UnrollUnnatural.Version
type nodes = {
diff --git a/src/plugins/wp/Strategy.ml b/src/plugins/wp/Strategy.ml
index b6073824dd1f12a63fc3e91e3d40f4575334e0c1..38f0f7f81414abd86eb784b79f6855821e19581b 100644
--- a/src/plugins/wp/Strategy.ml
+++ b/src/plugins/wp/Strategy.ml
@@ -106,7 +106,7 @@ type strategy = {
arguments : argument list ;
} and t = strategy
-let highest a b = Pervasives.compare b.priority a.priority
+let highest a b = Transitioning.Stdlib.compare b.priority a.priority
class pool =
object
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index a38694fad5d63641e00d86ef41b2af6b27f9ff8e..a06e4d093ddddfbe589c8c1c73955f0f2611cf8f 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -366,11 +366,11 @@ let compare p q =
in
let r = rank q.verdict - rank p.verdict in
if r <> 0 then r else
- let s = Pervasives.compare p.prover_steps q.prover_steps in
+ let s = Transitioning.Stdlib.compare p.prover_steps q.prover_steps in
if s <> 0 then s else
- let t = Pervasives.compare p.prover_time q.prover_time in
+ let t = Transitioning.Stdlib.compare p.prover_time q.prover_time in
if t <> 0 then t else
- Pervasives.compare p.solver_time q.solver_time
+ Transitioning.Stdlib.compare p.solver_time q.solver_time
let combine v1 v2 =
match v1 , v2 with
diff --git a/src/plugins/wp/Warning.ml b/src/plugins/wp/Warning.ml
index 56ea8e88b484eef4da87686ebfc3bd2894cf8b5d..e9bc3d515bf18c680d5b8f834b195f12f1ca1e71 100644
--- a/src/plugins/wp/Warning.ml
+++ b/src/plugins/wp/Warning.ml
@@ -48,7 +48,7 @@ struct
match w1.severe , w2.severe with
| true , false -> (-1)
| false , true -> 1
- | _ -> Pervasives.compare w1 w2
+ | _ -> Transitioning.Stdlib.compare w1 w2
end
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 34c76d1ff2e5b49184aab55d7def49df1df0ab4d..04cd9701c91426a98d40259689f9c518e9d46d0a 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -317,7 +317,7 @@ module AinfoComparable = struct
let c = !cmp obj_a obj_b in
if c <> 0 then c
else match a.arr_flat , b.arr_flat with
- | Some a , Some b -> Pervasives.compare a.arr_size b.arr_size
+ | Some a , Some b -> Transitioning.Stdlib.compare a.arr_size b.arr_size
| None , Some _ -> (-1)
| Some _ , None -> 1
| None , None -> 0
@@ -574,7 +574,7 @@ and compare_array_ptr_conflated a b =
let c = compare_ptr_conflated obj_a obj_b in
if c <> 0 then c
else match a.arr_flat , b.arr_flat with
- | Some a , Some b -> Pervasives.compare a.arr_size b.arr_size
+ | Some a , Some b -> Transitioning.Stdlib.compare a.arr_size b.arr_size
| None , Some _ -> (-1)
| Some _ , None -> 1
| None , None -> 0
diff --git a/src/plugins/wp/proof.ml b/src/plugins/wp/proof.ml
index 129c0aad1eef0dae724859a24e95067287cecfc3..5a314f37dd03e886b58b0e872d5b864f447586f9 100644
--- a/src/plugins/wp/proof.ml
+++ b/src/plugins/wp/proof.ml
@@ -225,7 +225,7 @@ let update_hints_for_goal goal hints =
try
let old_hints,script,qed = Hashtbl.find scriptbase goal in
let new_hints = List.sort String.compare hints in
- if Pervasives.compare new_hints old_hints <> 0 then
+ if Transitioning.Stdlib.compare new_hints old_hints <> 0 then
begin
Hashtbl.replace scriptbase goal (new_hints,script,qed) ;
needsave := true ;
diff --git a/src/plugins/wp/share/install.ml b/src/plugins/wp/share/install.ml
index 334e78760b39c685fd9e32b3ce9abe9e40e9de56..bb0ee0a194cece3b8fc548b37236ee8cd01bfba0 100644
--- a/src/plugins/wp/share/install.ml
+++ b/src/plugins/wp/share/install.ml
@@ -43,8 +43,8 @@ let hardcopy inc out =
begin
let buffer = Bytes.create 1024 in
let n = ref 0 in
- while (n := Pervasives.input inc buffer 0 1024 ; !n > 0) do
- Pervasives.output out buffer 0 !n
+ while (n := input inc buffer 0 1024 ; !n > 0) do
+ output out buffer 0 !n
done ;
flush out ;
end
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 7c2583caaf67aabc0f6133d09e4cb50880a1c166..7e3009c53bb7fe0117b0c4850da8094daff69536 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -192,7 +192,7 @@ let compare_kind k1 k2 = match k1, k2 with
if cmp <> 0 then cmp
else
Property.compare p1 p2
- | _,_ -> Pervasives.compare (kind_order k1) (kind_order k2)
+ | _,_ -> Transitioning.Stdlib.compare (kind_order k1) (kind_order k2)
let compare_prop_id pid1 pid2 =
(* This order of comparison groups together prop_pids with same properties *)
@@ -204,7 +204,7 @@ let compare_prop_id pid1 pid2 =
let cmp = compare_kind pid2.p_kind pid1.p_kind in
if cmp <> 0 then cmp
else
- Pervasives.compare pid1.p_part pid2.p_part
+ Transitioning.Stdlib.compare pid1.p_part pid2.p_part
module PropId =
Datatype.Make_with_collections(