From 441ca614653aa0a69d357a7933bba5b3f36984e0 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 9 May 2018 19:58:04 -0500 Subject: [PATCH] remove annoying spelling mistake --- src/sat/Sidekick_sat.ml | 2 +- src/sat/Theory_intf.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/Sidekick_sat.ml b/src/sat/Sidekick_sat.ml index 3eea13fa..3a3c0306 100644 --- a/src/sat/Sidekick_sat.ml +++ b/src/sat/Sidekick_sat.ml @@ -17,7 +17,7 @@ type ('formula, 'proof) res = ('formula, 'proof) Theory_intf.res = (** The current set of assumptions is satisfiable. *) | Unsat of 'formula list * 'proof (** 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. *) (** 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. *) diff --git a/src/sat/Theory_intf.ml b/src/sat/Theory_intf.ml index ce2d6b96..16e9c073 100644 --- a/src/sat/Theory_intf.ml +++ b/src/sat/Theory_intf.ml @@ -36,7 +36,7 @@ type ('formula, 'proof) res = (** The current set of assumptions is satisfiable. *) | Unsat of 'formula list * 'proof (** 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. *) (** Actions given to the theory during initialization, to be used