diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index 8a58c75e..8d9caf41 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -16,6 +16,7 @@ module Make (A: CC_ARG)
   : S with module T = A.T
        and module Lit = A.Lit
        and type proof = A.proof
+       and type step_id = A.step_id
        and module Actions = A.Actions
 = struct
   module T = A.T
@@ -27,7 +28,8 @@ module Make (A: CC_ARG)
   type lit = Lit.t
   type fun_ = T.Fun.t
   type proof = A.proof
-  type dproof = proof -> unit
+  type step_id = A.step_id
+  type pstep = proof -> step_id
   type actions = Actions.t
 
   module Term = T.Term
diff --git a/src/cc/Sidekick_cc.mli b/src/cc/Sidekick_cc.mli
index 8e9cdb95..2d0bb9f8 100644
--- a/src/cc/Sidekick_cc.mli
+++ b/src/cc/Sidekick_cc.mli
@@ -7,4 +7,5 @@ module Make (A: CC_ARG)
   : S with module T = A.T
        and module Lit = A.Lit
        and type proof = A.proof
+       and type step_id = A.step_id
        and module Actions = A.Actions