X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fformula.mli;h=6c54386e212f43d74dcd4e29d1e315fadfd88d62;hp=e108758b84859e7823ade7dc355f92d4999dda5c;hb=83c90cb5eeebfffa05d0383430eb80e7905b46a0;hpb=c1b43e1dcdb3d0960dbc50db9f226d68ad30c16e

diff --git a/src/formula.mli b/src/formula.mli
index e108758..6c54386 100644
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -53,7 +53,10 @@ val size : t -> int
 (** Syntactic size of the formula *)
 
 val eval_form : (StateSet.t * StateSet.t) -> t -> bool
-(** [eval_form s_1,s_2 F] evaluates the formula [F] on [(s_1,s_2)] *)
+(** [eval_form sf,sn F] evaluates the formula [F] on [(sf,sn)] *)
+
+val infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> t -> bool
+(** [eval_form S1 S2 F] infers S1; S2 |- F *)
 
 val print : Format.formatter -> t -> unit
 (** Pretty printer *)