From 6f7f2b2823f788ffc0eaeb03d9149ec22d15755d Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 20 Jul 2021 00:35:49 -0400 Subject: [PATCH] fix doc --- src/sat/Solver_intf.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index afe2dfc6..93efc583 100644 --- a/src/sat/Solver_intf.ml +++ b/src/sat/Solver_intf.ml @@ -63,6 +63,7 @@ type negated = (** This type is used during the normalisation of formulas. See {!val:Expr_intf.S.norm} for more details. *) +(** The type of reasons for propagations of a formula [f]. *) type ('formula, 'proof) reason = | Consequence of (unit -> 'formula list * 'proof) [@@unboxed] (** [Consequence (l, p)] means that the formulas in [l] imply the propagated @@ -83,7 +84,6 @@ type ('formula, 'proof) reason = propagating, and then use [Consequence (fun () -> expl, proof)] with the already produced [(expl,proof)] tuple. *) -(** The type of reasons for propagations of a formula [f]. *) type lbool = L_true | L_false | L_undefined (** Valuation of an atom *)