From 55c5c3f0f038eb2531e6c694fec0616d4d1a05eb Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 12 Nov 2014 23:39:04 +0100 Subject: [PATCH] Fix in doc --- sat/theory_intf.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sat/theory_intf.ml b/sat/theory_intf.ml index 023ef750..0463901a 100644 --- a/sat/theory_intf.ml +++ b/sat/theory_intf.ml @@ -30,7 +30,7 @@ module type S = sig (** The type for a slice of litterals to assume/propagate in the theory. [get] operations should only be used for integers [ start <= i < start + length]. The semantic for push is the following : - [push f \[a1; a2;... ; an\] p] shoudl be so that p is a proof of + [push f \[a1; a2;... ; an\] p] should be so that [p] is a proof of a1 /\ a2 /\ ... /\ an => f. *) type level