X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fauto%2Fformula.mli;fp=src%2Fauto%2Fformula.mli;h=2421d515d076873e4d04e1b04b8bc07ce9928ccd;hp=78df01c72361527f1e066de0a420f779d31b81d4;hb=35c32fbd2543a399cc6939f21317bebf37172646;hpb=cd87d0f43eb81563fd303875ff4c83fe382ea99f

diff --git a/src/auto/formula.mli b/src/auto/formula.mli
index 78df01c..2421d51 100644
--- a/src/auto/formula.mli
+++ b/src/auto/formula.mli
@@ -14,30 +14,28 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-04 22:47:09 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-09 11:13:06 CET by Kim Nguyen>
 *)
 
-module type PREDICATE =
+module type ATOM =
 sig
   type t
-  type ctx
-  val eval : ctx -> t -> bool
   val neg : t -> t
   include Utils.Hcons.Abstract with type t := t
   include Utils.Common_sig.Printable with type t := t
 end
 
-type ('formula,'pred) expr =
+type ('formula,'atom) expr =
   | False
   | True
   | Or of 'formula * 'formula
   | And of 'formula * 'formula
-  | Atom of 'pred
+  | Atom of 'atom
 
 (** View of the internal representation of a formula,
     used for pattern matching *)
 
-module Make(P : PREDICATE) :
+module Make(P : ATOM) :
 sig
   type t
 
@@ -86,6 +84,4 @@ sig
   val of_bool : bool -> t
   (** Convert an ocaml Boolean value to a formula *)
 
-  val eval : P.ctx -> t -> bool
-    (** Evaluate a formula given a context for atomic predicates *)
 end