diff --git a/src/core/Binder.ml b/src/core/Binder.ml index 99dd2addb..2d266ac75 100644 --- a/src/core/Binder.ml +++ b/src/core/Binder.ml @@ -14,7 +14,7 @@ let exists = Exists let lambda = Lambda let forall_ty = ForallTy -let compare (a:t) b = CCShims_.Stdlib.compare a b +let compare (a:t) b = Stdlib.compare a b let equal (a:t) b = a=b let hash (a:t) = Hashtbl.hash a diff --git a/src/core/Builtin.ml b/src/core/Builtin.ml index 845e1a7f7..d58be4117 100644 --- a/src/core/Builtin.ml +++ b/src/core/Builtin.ml @@ -317,7 +317,7 @@ module Tag = struct | T_ac of ID.t (** AC symbols *) | T_cannot_orphan - let compare = CCShims_.Stdlib.compare + let compare = Stdlib.compare let pp out = function | T_lia -> Fmt.string out "lia" diff --git a/src/core/Comparison.ml b/src/core/Comparison.ml index 9347abf77..a2db85c66 100644 --- a/src/core/Comparison.ml +++ b/src/core/Comparison.ml @@ -8,7 +8,7 @@ type t = Lt | Leq | Eq | Geq | Gt | Incomparable type comparison = t -let equal : t -> t -> bool = CCShims_.Stdlib.(=) +let equal : t -> t -> bool = Stdlib.(=) let to_string = function | Lt -> "<" diff --git a/src/core/Dtree.ml b/src/core/Dtree.ml index a66e3832d..1dcd8e81f 100644 --- a/src/core/Dtree.ml +++ b/src/core/Dtree.ml @@ -38,7 +38,7 @@ let compare_char c1 c2 = | Symbol s1, Symbol s2 -> ID.compare s1 s2 | Variable v1, Variable v2 -> compare_vars v1 v2 | Subterm t1, Subterm t2 -> T.compare t1 t2 - | _ -> CCShims_.Stdlib.compare (char_to_int_ c1) (char_to_int_ c2) + | _ -> Stdlib.compare (char_to_int_ c1) (char_to_int_ c2) let[@inline] eq_char c1 c2 = compare_char c1 c2 = 0 diff --git a/src/core/ID.ml b/src/core/ID.ml index ffad45ee6..b4dcf5074 100644 --- a/src/core/ID.ml +++ b/src/core/ID.ml @@ -66,7 +66,7 @@ let payload_pred ~f:p t = let hash t = t.id let equal i1 i2 = i1.id = i2.id -let compare i1 i2 = CCShims_.Stdlib.compare i1.id i2.id +let compare i1 i2 = Stdlib.compare i1.id i2.id let pp out id = CCFormat.string out id.name let to_string = CCFormat.to_string pp diff --git a/src/core/InnerTerm.ml b/src/core/InnerTerm.ml index e9d639aa6..6a985a885 100644 --- a/src/core/InnerTerm.ml +++ b/src/core/InnerTerm.ml @@ -118,7 +118,7 @@ let[@inline] ty_exn t = match t.ty with let[@inline] hash t = Hash.int t.id let[@inline] equal : t -> t -> bool = fun t1 t2 -> t1 == t2 -let[@inline] compare t1 t2 = CCShims_.Stdlib.compare t1.id t2.id +let[@inline] compare t1 t2 = Stdlib.compare t1.id t2.id let rec same_l_rec l1 l2 = match l1, l2 with | [], [] -> true diff --git a/src/core/Literal.ml b/src/core/Literal.ml index 9a63f7b7a..e26f54e1b 100644 --- a/src/core/Literal.ml +++ b/src/core/Literal.ml @@ -64,7 +64,7 @@ let compare l1 l2 = if c <> 0 then c else let c = T.compare r1 r2 in if c <> 0 then c else - CCShims_.Stdlib.compare sign1 sign2 + Stdlib.compare sign1 sign2 | True, True | False, False -> 0 | _, _ -> __to_int l1 - __to_int l2 @@ -718,7 +718,7 @@ module Comp = struct | True -> 0 | Equation _ -> 30 in - C.of_total (CCShims_.Stdlib.compare (_to_int l1) (_to_int l2)) + C.of_total (Stdlib.compare (_to_int l1) (_to_int l2)) (* by multiset of terms *) let _cmp_by_term_multiset ~ord l1 l2 = diff --git a/src/core/Literals.ml b/src/core/Literals.ml index 21dd9edcc..b48302faf 100644 --- a/src/core/Literals.ml +++ b/src/core/Literals.ml @@ -113,7 +113,7 @@ let neg lits = module MLI = Multiset.Make(struct type t = Lit.t * int let compare (l1,i1)(l2,i2) = - if i1 = i2 then Lit.compare l1 l2 else CCShims_.Stdlib.compare i1 i2 + if i1 = i2 then Lit.compare l1 l2 else Stdlib.compare i1 i2 end) let _compare_lit_with_idx ~ord (lit1,i1) (lit2,i2) = diff --git a/src/core/Ordering.ml b/src/core/Ordering.ml index 56118de34..1af86b820 100644 --- a/src/core/Ordering.ml +++ b/src/core/Ordering.ml @@ -1058,7 +1058,7 @@ module LambdaKBO : ORD = struct module WH = CCHashtbl.Make(struct type t = W.t - let equal = CCShims_.Stdlib.(=) + let equal = Stdlib.(=) let hash = W.hash end) diff --git a/src/core/Position.ml b/src/core/Position.ml index 4c8ca2ba6..842a0bcf3 100644 --- a/src/core/Position.ml +++ b/src/core/Position.ml @@ -23,7 +23,7 @@ let head pos = Head pos let arg i pos = Arg (i, pos) let body pos = Body pos -let compare = CCShims_.Stdlib.compare +let compare = Stdlib.compare let equal p1 p2 = compare p1 p2 = 0 let hash p = Hashtbl.hash p diff --git a/src/core/STerm.ml b/src/core/STerm.ml index 2e45ff30e..6c622b49d 100644 --- a/src/core/STerm.ml +++ b/src/core/STerm.ml @@ -55,7 +55,7 @@ let to_int_ = function | With _ -> 12 let rec compare t1 t2 = match t1.term, t2.term with - | Var s1, Var s2 -> CCShims_.Stdlib.compare s1 s2 + | Var s1, Var s2 -> Stdlib.compare s1 s2 | Const s1, Const s2 -> String.compare s1 s2 | App (s1,l1), App (s2, l2) -> let c = compare s1 s2 in @@ -109,7 +109,7 @@ and compare_typed_var (v1,o1)(v2,o2) = let cmp = compare in CCOrd.( compare_var v1 v2 (Util.ord_option cmp, o1, o2) ) -and compare_var : var CCOrd.t = CCShims_.Stdlib.compare +and compare_var : var CCOrd.t = Stdlib.compare let equal t1 t2 = compare t1 t2 = 0 diff --git a/src/core/Scoped.ml b/src/core/Scoped.ml index 93c81e61e..3994dae90 100644 --- a/src/core/Scoped.ml +++ b/src/core/Scoped.ml @@ -22,7 +22,7 @@ let map f (v,i) : _ t = (f v, i) let[@inline] equal eq (v1:_ t) (v2:_ t) : bool = scope v1 = scope v2 && eq (get v1) (get v2) let compare c v1 v2 = if scope v1 = scope v2 then c (get v1) (get v2) - else CCShims_.Stdlib.compare (scope v1) (scope v2) + else Stdlib.compare (scope v1) (scope v2) let hash f (v,sc) = Hash.combine2 (Hash.int sc) (f v) diff --git a/src/core/Statement.ml b/src/core/Statement.ml index cafeab2af..2f789dcbe 100644 --- a/src/core/Statement.ml +++ b/src/core/Statement.ml @@ -5,7 +5,7 @@ module OptionSet = Set.Make( struct - let compare x y = CCShims_.Stdlib.compare x y + let compare x y = Stdlib.compare x y type t = int option end) diff --git a/src/parsers/trace_tstp.ml b/src/parsers/trace_tstp.ml index 409f09c33..d1e1773ac 100644 --- a/src/parsers/trace_tstp.ml +++ b/src/parsers/trace_tstp.ml @@ -47,7 +47,7 @@ let hash p = match p with | InferForm (_, lazy s) | InferClause (_, lazy s) -> Hashtbl.hash s.id -let compare p1 p2 = CCShims_.Stdlib.compare p1 p2 (* FIXME *) +let compare p1 p2 = Stdlib.compare p1 p2 (* FIXME *) (** {2 Constructors and utils} *) diff --git a/src/prover/SClause.ml b/src/prover/SClause.ml index aaa3c2444..9b098bb05 100644 --- a/src/prover/SClause.ml +++ b/src/prover/SClause.ml @@ -31,7 +31,7 @@ let make ~trail lits = { lits; trail; id; flags=0; } let[@inline] equal c1 c2 = c1.id = c2.id -let[@inline] compare c1 c2 = CCShims_.Stdlib.compare c1.id c2.id +let[@inline] compare c1 c2 = Stdlib.compare c1.id c2.id let[@inline] id c = c.id let[@inline] hash c = Hash.int c.id let[@inline] lits c = c.lits diff --git a/src/prover/stream.ml b/src/prover/stream.ml index 47eece5fe..929d2e144 100644 --- a/src/prover/stream.ml +++ b/src/prover/stream.ml @@ -45,7 +45,7 @@ module Make(A:ARG) = struct () let equal s1 s2 = s1.id = s2.id - let compare s1 s2 = CCShims_.Stdlib.compare s1.id s2.id + let compare s1 s2 = Stdlib.compare s1.id s2.id let id s = s.id let hash s = Hashtbl.hash s.id diff --git a/src/tools/cnf_of.ml b/src/tools/cnf_of.ml index 0f770c4ca..cb9a5f16d 100644 --- a/src/tools/cnf_of.ml +++ b/src/tools/cnf_of.ml @@ -26,7 +26,7 @@ let options = ; "--time-limit", Arg.Int Util.set_time_limit, " hard time limit (in s)" ; "--print-input", Arg.Set print_in, " print input problem" ] @ Options.make () - |> List.sort CCShims_.Stdlib.compare + |> List.sort Stdlib.compare |> Arg.align let print_res (decls: _ CCVector.ro_vector) : unit = diff --git a/src/tools/problem_features.ml b/src/tools/problem_features.ml index 19e784e1d..3fa2ca0df 100644 --- a/src/tools/problem_features.ml +++ b/src/tools/problem_features.ml @@ -275,7 +275,7 @@ let cnf_features = ref true let options = [ "--cnf-features", Arg.Bool ((:=) cnf_features), " clausify the problem and include CNF features"] @ Options.make () - |> List.sort CCShims_.Stdlib.compare + |> List.sort Stdlib.compare |> Arg.align (* process the given file, converting it to CNF *)