remove most proof-trace code

src/proof-trace/dummy/Sidekick_proof_trace_dummy.ml

@@ -1,35 +0,0 @@
-(** Dummy proof traces.
-
-    These proof traces will not record information. *)
-
-module type S = Sidekick_sigs_proof_trace.S
-
-module type ARG = sig
-  include Sidekick_sigs_proof_trace.ARG
-
-  val dummy_step_id : step_id
-end
-
-module Make (A : ARG) : S with type t = unit and module A = A = struct
-  module A = A
-
-  type t = unit
-
-  let enabled _ = false
-  let add_step _ _ = A.dummy_step_id
-  let add_unsat _ _ = ()
-  let delete _ _ = ()
-end
-
-(** Dummy proof trace where everything is [unit]. Use this if you don't care
-   for proofs at all. *)
-module Unit :
-  S with type t = unit and type A.rule = unit and type A.step_id = unit =
-Make (struct
-  type rule = unit
-  type step_id = unit
-
-  module Step_vec = Vec_unit
-
-  let dummy_step_id = ()
-end)

src/proof-trace/dummy/dune

@@ -1,6 +0,0 @@
-(library
- (name sidekick_proof_trace_dummy)
- (public_name sidekick.proof-trace.dummy)
- (synopsis "Dummy proof trace that stores nothing")
- (libraries sidekick.util sidekick.sigs.proof-trace)
- (flags :standard -open Sidekick_util))

src/proof-trace/dyn/Sidekick_proof_trace_dyn.ml

@@ -1,23 +0,0 @@
-module type ARG = Sidekick_sigs_proof_trace.ARG
-module type S = Sidekick_sigs_proof_trace.S
-
-(** Dynamic version.
-
-    The proof trace is a first-class module that can be provided at runtime. *)
-module Make_dyn (A : ARG) : S with module A = A = struct
-  module A = A
-
-  module type DYN = sig
-    val enabled : unit -> bool
-    val add_step : A.rule -> A.step_id
-    val add_unsat : A.step_id -> unit
-    val delete : A.step_id -> unit
-  end
-
-  type t = (module DYN)
-
-  let[@inline] enabled ((module Tr) : t) : bool = Tr.enabled ()
-  let[@inline] add_step ((module Tr) : t) rule : A.step_id = Tr.add_step rule
-  let[@inline] add_unsat ((module Tr) : t) s : unit = Tr.add_unsat s
-  let[@inline] delete ((module Tr) : t) s : unit = Tr.delete s
-end

src/proof-trace/dyn/dune

@@ -1,6 +0,0 @@
-(library
- (name sidekick_proof_trace_dyn)
- (public_name sidekick.proof-trace.dyn)
- (synopsis "Dynamic version of the proof trace")
- (libraries sidekick.util sidekick.sigs.proof-trace)
- (flags :standard -open Sidekick_util))