X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fformula.ml;h=8369571bfa33172e4b7c53a3209af7eceb2824eb;hp=c75748fb6ef9ebe56b13aa8438930d872ea27561;hb=d0dc6fbd661c7a79a2d8f875a204f587e6a5162d;hpb=83c90cb5eeebfffa05d0383430eb80e7905b46a0 diff --git a/src/formula.ml b/src/formula.ml index c75748f..8369571 100644 --- a/src/formula.ml +++ b/src/formula.ml @@ -91,7 +91,7 @@ let rec infer_form ssq ssr f = match expr f with | Atom(dir, b, s) -> let setq, setr = match dir with |`Left -> fst ssq, fst ssr - | `Right -> snd ssq, fst ssr in + | `Right -> snd ssq, snd ssr in (* WG: WE SUPPOSE THAT Q^r and Q^q are disjoint ! *) let mem = StateSet.mem s setq || StateSet.mem s setr in if b then mem else not mem