simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 12:24:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

missing change

Browse source
This commit is contained in:
Simon Cruanes 2016-04-15 14:05:42 +02:00
parent 1ce3973f9e
commit 22ebead17a
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.mli
View file

@ -14,8 +14,8 @@
module type S = Solver_intf.S module type S = Solver_intf.S
(** Simple case where the proof type is [unit] and the theory is empty *) (** Simple case where the proof type is [unit] and the theory is empty *)
module DummyTheory(F : Formula_intf.S with type proof = unit) : module DummyTheory(F : Formula_intf.S) :
Theory_intf.S with type formula = F.t and type proof = unit Theory_intf.S with type formula = F.t and type proof = F.proof
module Make (F : Formula_intf.S) module Make (F : Formula_intf.S)
(Th : Theory_intf.S with type formula = F.t and type proof = F.proof) (Th : Theory_intf.S with type formula = F.t and type proof = F.proof)