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

style

Browse source
This commit is contained in:
Simon Cruanes 2015-11-25 10:28:21 +01:00
parent 15e5a4224d
commit 99b1f25e4f
2 changed files with 10 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
solver/internal.ml
View file

@ -4,8 +4,11 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes Copyright 2014 Simon Cruanes
*) *)
module Make (L : Log_intf.S)(St : Solver_types.S) module Make
(Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof) = struct (L : Log_intf.S)
(St : Solver_types.S)
(Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
= struct
module Proof = Res.Make(L)(St) module Proof = Res.Make(L)(St)

7
solver/internal.mli
View file

@ -4,8 +4,11 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes Copyright 2014 Simon Cruanes
*) *)
module Make (L : Log_intf.S)(St : Solver_types.S) module Make
(Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof) : sig (L : Log_intf.S)
(St : Solver_types.S)
(Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
: sig
(** Functor to create a solver parametrised by the atomic formulas and a theory. *) (** Functor to create a solver parametrised by the atomic formulas and a theory. *)
exception Unsat exception Unsat