From 8ae3277cb329466ba3ea64d246e97635c0ca5343 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 14 Nov 2014 17:59:50 +0100 Subject: [PATCH] Fixed a bug in documentaion placement in html --- sat/theory_intf.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/sat/theory_intf.ml b/sat/theory_intf.ml index 0463901a..81b02cd8 100644 --- a/sat/theory_intf.ml +++ b/sat/theory_intf.ml @@ -36,13 +36,13 @@ module type S = sig type level (** The type for levels to allow backtracking. *) - type res = - | Sat of level - | Unsat of formula list * proof (** Type returned by the theory, either the current set of assumptions is satisfiable, or it is not, in which case a tautological clause (hopefully minimal) is returned. Formulas in the unsat clause must come from the current set of assumptions, i.e must have been encountered in a slice. *) + type res = + | Sat of level + | Unsat of formula list * proof val dummy : level (** A dummy level. *)