simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fixed a bug in documentaion placement in html

Browse source
This commit is contained in:
Guillaume Bury 2014-11-14 17:59:50 +01:00
parent fcbcf5a9d4
commit 8ae3277cb3
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
sat/theory_intf.ml
View file

@ -36,13 +36,13 @@ module type S = sig
type level type level
(** The type for levels to allow backtracking. *) (** 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, (** 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. 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 Formulas in the unsat clause must come from the current set of assumptions, i.e
must have been encountered in a slice. *) must have been encountered in a slice. *)
type res =
| Sat of level
| Unsat of formula list * proof
val dummy : level val dummy : level
(** A dummy level. *) (** A dummy level. *)