From 7749f7aaacbd50ca812b0e6bdecb361baeaa3570 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 25 Aug 2017 19:15:12 +0200 Subject: [PATCH] Manual re-indent --- src/core/plugin_intf.ml | 7 +++---- src/core/solver_types_intf.ml | 4 ++-- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src/core/plugin_intf.ml b/src/core/plugin_intf.ml index c4dd3839..92d1b2e4 100644 --- a/src/core/plugin_intf.ml +++ b/src/core/plugin_intf.ml @@ -27,8 +27,7 @@ type 'term eval_res = | Unknown (** The given formula does not have an evaluation *) | Valued of bool * ('term list) (** The given formula can be evaluated to the given bool. The list of terms to give is the list of terms that - were effectively used for the evaluation. - *) + were effectively used for the evaluation. *) (** The type of evaluation results for a given formula. For instance, let's suppose we want to evaluate the formula [x * y = 0], the following result are correct: @@ -67,8 +66,8 @@ type ('term, 'formula, 'proof) slice = { Should only be called on integers [i] s.t. [start <= i < start + length] *) push : 'formula list -> 'proof -> unit; (** Add a clause to the solver. *) - propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit; - (** Propagate a formula, i.e. the theory can + propagate : 'formula -> + ('term, 'formula, 'proof) reason -> unit; (** Propagate a formula, i.e. the theory can evaluate the formula to be true (see the definition of {!type:eval_res} *) } diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml index 0dbebffd..e9832e14 100644 --- a/src/core/solver_types_intf.ml +++ b/src/core/solver_types_intf.ml @@ -119,7 +119,7 @@ module type S = sig (** {2 Decisions and propagations} *) type t = | Lit of lit - | Atom of atom + | Atom of atom (**) (** Either a lit of an atom *) val of_lit : lit -> t @@ -130,7 +130,7 @@ module type S = sig type elt = | E_lit of lit - | E_var of var + | E_var of var (**) (** Either a lit of a var *) val nb_elt : unit -> int