simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: adapt CC to new proofs

Browse source
This commit is contained in:
Simon Cruanes 2021-09-29 22:19:16 -04:00
parent df40b5a5c1
commit 04f1ba063d
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
2 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/cc/Sidekick_cc.ml
View file

@ -16,6 +16,7 @@ module Make (A: CC_ARG)
: S with module T = A.T : S with module T = A.T
and module Lit = A.Lit and module Lit = A.Lit
and type proof = A.proof and type proof = A.proof
and type step_id = A.step_id
and module Actions = A.Actions and module Actions = A.Actions
= struct = struct
module T = A.T module T = A.T
@ -27,7 +28,8 @@ module Make (A: CC_ARG)
type lit = Lit.t type lit = Lit.t
type fun_ = T.Fun.t type fun_ = T.Fun.t
type proof = A.proof type proof = A.proof
type dproof = proof -> unit type step_id = A.step_id
type pstep = proof -> step_id
type actions = Actions.t type actions = Actions.t
module Term = T.Term module Term = T.Term

1
src/cc/Sidekick_cc.mli
View file

@ -7,4 +7,5 @@ module Make (A: CC_ARG)
: S with module T = A.T : S with module T = A.T
and module Lit = A.Lit and module Lit = A.Lit
and type proof = A.proof and type proof = A.proof
and type step_id = A.step_id
and module Actions = A.Actions and module Actions = A.Actions