diff --git a/solver/internal.ml b/solver/internal.ml index a3a32ada..57b84cf7 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -4,8 +4,11 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module Make (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 Make + (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) diff --git a/solver/internal.mli b/solver/internal.mli index 89e94f4b..07670ef5 100644 --- a/solver/internal.mli +++ b/solver/internal.mli @@ -4,8 +4,11 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module Make (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 +module Make + (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. *) exception Unsat