diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 949e1230..ce6275fa 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -146,8 +146,6 @@ module Make (A: CC_ARG) let[@inline] set_field f b t = t.n_bits <- Bits.set f b t.n_bits end - module N_tbl = CCHashtbl.Make(N) - (* non-recursive, inlinable function for [find] *) let[@inline] find_ (n:node) : repr = let n2 = n.n_root in diff --git a/src/drup/sidekick_drup.ml b/src/drup/sidekick_drup.ml index cbe0d992..70e47de8 100644 --- a/src/drup/sidekick_drup.ml +++ b/src/drup/sidekick_drup.ml @@ -128,7 +128,6 @@ module Make() : S = struct val pp : t Fmt.printer val of_list : store -> atom list -> t val of_iter : store -> atom Iter.t -> t - module Set : CCSet.S with type elt = t module Tbl : CCHashtbl.S with type key = t end = struct type t = { @@ -171,7 +170,6 @@ module Make() : S = struct let[@inline] equal a b = a.id = b.id let[@inline] compare a b = compare a.id b.id end - module Set = CCSet.Make(As_key) module Tbl = CCHashtbl.Make(As_key) end type clause = Clause.t diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index c8c0cf04..e7537f05 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -28,10 +28,8 @@ module Make(Plugin : PLUGIN) (* a boolean variable (positive int) *) module Var0 : sig include Int_id.S - module Set : Set.S with type elt = t end = struct include Int_id.Make() - module Set = Util.Int_set end type var = Var0.t @@ -46,7 +44,6 @@ module Make(Plugin : PLUGIN) val abs : t -> t val pa : var -> t val na : var -> t - module Set : CCSet.S with type elt = t end = struct include Int_id.Make() let[@inline] neg i = (i lxor 1) @@ -57,7 +54,6 @@ module Make(Plugin : PLUGIN) let[@inline] abs a = a land (lnot 1) let[@inline] var a = Var0.of_int_unsafe (a lsr 1) let[@inline] na v = (((v:var:>int) lsl 1) lor 1) - module Set = Util.Int_set end type atom = Atom0.t @@ -213,7 +209,7 @@ module Make(Plugin : PLUGIN) let[@inline] pp_sign a = if sign a then "+" else "-" (* print level+reason of assignment *) - let debug_reason self out = function + let debug_reason _self out = function | n, _ when n < 0 -> Format.fprintf out "%%" | n, None -> Format.fprintf out "%d" n | n, Some Decision -> Format.fprintf out "@@%d" n @@ -1890,7 +1886,6 @@ module Make(Plugin : PLUGIN) let module M = struct type nonrec lit = lit type clause = Clause.t - type proof = Proof.t let unsat_conflict = unsat_conflict let unsat_assumptions = unsat_assumptions end in diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 51a3b42d..26392232 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -34,9 +34,6 @@ module type DATA_TY = sig val view : t -> (cstor, t) data_ty_view val cstor_args : cstor -> t Iter.t - - (** A table indexed by types. *) - module Tbl : Hashtbl.S with type key = t end (** {2 Cardinality of types} *) @@ -200,7 +197,6 @@ module Make(A : ARG) : S with module A = A = struct module T = A.S.T.Term module N = SI.CC.N module Ty = A.S.T.Ty - module Fun = A.S.T.Fun module Expl = SI.CC.Expl module Card = Compute_card(A)