prerr_endline ("path: " ^ String.concat ","
(List.map string_of_int p1));
prerr_endline ("path: " ^ String.concat ","
(List.map string_of_int p1));
- let _, lit, vl, proof = Terms.M.find id bag in
+ 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 lit =match lit with
| Terms.Predicate t -> assert false
| Terms.Equation (l,r,ty,_) ->
if ongoal then id1,id,get_literal id1
else id,id1,(lit,vl,proof)
in
if ongoal then id1,id,get_literal id1
else id,id1,(lit,vl,proof)
in