From d538e19411a5fc1a73f0d8b16f42dd79d206d6e0 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 17 Jan 2017 15:59:29 +0100 Subject: [PATCH] Fix typo of Plugin_intf.reason --- src/core/plugin_intf.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/core/plugin_intf.ml b/src/core/plugin_intf.ml index 8ff1cdbd..60b546ac 100644 --- a/src/core/plugin_intf.ml +++ b/src/core/plugin_intf.ml @@ -54,12 +54,11 @@ type ('term, 'formula) assumption = (** Asusmptions made by the core SAT solver. *) type ('term, 'formula, 'proof) reason = - | Eval of 'term list - | Consequence of 'formula list * 'proof -(** The type of reasons for propagations of a formula [f]. - [Semantic lvl] means that [f] is true because of the assignments whose level is [<= lvl]. - [Consequence (l, p)] means that the formulas in [l] imply [f]. The proof should be a proof - of the clause "[l] implies [f]". *) + | Eval of 'term list (** The formula can be evalutaed using the terms in the list *) + | Consequence of 'formula list * 'proof (** [Consequence (l, p)] means that the formulas in [l] imply + the propagated formula [f]. The proof should be a proof of + the clause "[l] implies [f]". *) +(** The type of reasons for propagations of a formula [f]. *) type ('term, 'formula, 'proof) slice = { start : int; (** Start of the slice *)