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

Merge pull request #2 from Gbury/refactor

Browse source 
Indentation and style fix
This commit is contained in:
Guillaume Bury 2015-11-25 14:01:29 +01:00
commit f72f3c44ee
22 changed files with 657 additions and 651 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