From 04f1ba063d684c43ccfdd8344c4e4524e3cd49c3 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 29 Sep 2021 22:19:16 -0400 Subject: [PATCH] wip: adapt CC to new proofs --- src/cc/Sidekick_cc.ml | 4 +++- src/cc/Sidekick_cc.mli | 1 + 2 files changed, 4 insertions(+), 1 deletion(-) 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