t vl
in
let get_literal id =
- let (_, lit, vl, proof),_,_ = Terms.get_from_bag id bag in
- let lit =match lit with
- | Terms.Predicate t -> assert false
- | Terms.Equation (l,r,ty,_) ->
+ let (_, nlit, plit, vl, proof),_,_ = Terms.get_from_bag id bag in
+ let lit = match nlit,plit with
+ | [],[Terms.Equation (l,r,ty,_),_] ->
Terms.Node [ Terms.Leaf eqP(); ty; l; r]
+ | _ -> assert false
in
lit, vl, proof
in