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

remove annoying spelling mistake

Browse source
This commit is contained in:
Simon Cruanes 2018-05-09 19:58:04 -05:00
parent c44e9bc16d
commit 441ca61465
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/Sidekick_sat.ml
View file

@ -17,7 +17,7 @@ type ('formula, 'proof) res = ('formula, 'proof) Theory_intf.res =
(** The current set of assumptions is satisfiable. *) (** The current set of assumptions is satisfiable. *)
| Unsat of 'formula list * 'proof | Unsat of 'formula list * 'proof
(** The current set of assumptions is *NOT* satisfiable, and here is a (** The current set of assumptions is *NOT* satisfiable, and here is a
theory tautology (with its proof), for which every litteral is false theory tautology (with its proof), for which every literal is false
under the current assumptions. *) under the current assumptions. *)
(** Type returned by the theory. Formulas in the unsat clause must come from the (** Type returned by the theory. Formulas in the unsat clause must come from the
current set of assumptions, i.e must have been encountered in a slice. *) current set of assumptions, i.e must have been encountered in a slice. *)

2
src/sat/Theory_intf.ml
View file

@ -36,7 +36,7 @@ type ('formula, 'proof) res =
(** The current set of assumptions is satisfiable. *) (** The current set of assumptions is satisfiable. *)
| Unsat of 'formula list * 'proof | Unsat of 'formula list * 'proof
(** The current set of assumptions is *NOT* satisfiable, and here is a (** The current set of assumptions is *NOT* satisfiable, and here is a
theory tautology (with its proof), for which every litteral is false theory tautology (with its proof), for which every literal is false
under the current assumptions. *) under the current assumptions. *)
(** Actions given to the theory during initialization, to be used (** Actions given to the theory during initialization, to be used