From 99b1f25e4fc4db71e8ce917ca7f1e81c1f8037f6 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 25 Nov 2015 10:28:21 +0100 Subject: [PATCH] style --- solver/internal.ml | 7 +++++-- solver/internal.mli | 7 +++++-- 2 files changed, 10 insertions(+), 4 deletions(-) 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