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

[feature] Allow arbitrary proof types in DummyTheory

Browse source
This commit is contained in:
Guillaume Bury 2016-04-15 14:02:18 +02:00
parent 2e6ff522e5
commit 1ce3973f9e
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
solver/solver.ml
View file

@ -12,12 +12,12 @@
module type S = Solver_intf.S module type S = Solver_intf.S
module DummyTheory(F : Formula_intf.S with type proof = unit) = struct module DummyTheory(F : Formula_intf.S) = struct
(* We don't have anything to do since the SAT Solver already (* We don't have anything to do since the SAT Solver already
* does propagation and conflict detection *) * does propagation and conflict detection *)
type formula = F.t type formula = F.t
type proof = unit type proof = F.proof
type level = unit type level = unit
type slice = { type slice = {