X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fformula.mli;h=9b2659f310575a5f1cb0b5b967c57057b3fcb472;hb=cb29d45b3a79233581292a2ef172151b1ff489cb;hp=46cbe6508c5219513329ebc404be212edaa77d98;hpb=cba2938d929fd5119b1491686ddc224d5af618c6;p=tatoo.git

diff --git a/src/formula.mli b/src/formula.mli
index 46cbe65..9b2659f 100644
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -18,17 +18,19 @@
 type move = [ `Left |`Right ]
 (** Direction for automata predicates *)
 
-type 'hcons expr =
-    False
-    | True
-    | Or of 'hcons * 'hcons
-    | And of 'hcons * 'hcons
-    | Atom of (move * bool * State.t)
-
-(** Partial internal representation of a formula,
+type 'formula expr =
+  | False
+  | True
+  | Or of 'formula * 'formula
+  | And of 'formula * 'formula
+  | Move of (move * bool * State.t)
+  | Label of QNameSet.t
+
+(** View of the internal representation of a formula,
     used for pattern matching *)
 
 type t
+
 (** Abstract type representing hashconsed formulae *)
 
 val hash : t -> int
@@ -43,8 +45,9 @@ val equal : t -> t -> bool
 val expr : t -> t expr
 (** Equality over formulae *)
 
-val st : t -> StateSet.t * StateSet.t
+(*val st : t -> StateSet.t * StateSet.t
 (** states occuring left and right, positively or negatively *)
+*)
 
 val compare : t -> t -> int
 (** Comparison of formulae *)