let p = Subst.apply_subst subst p in
Terms.Predicate p
in
- let nlit = List.map apply_subst_on_lit nlit in
- let plit = List.map apply_subst_on_lit plit in
+ let nlit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) nlit in
+ let plit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) plit in
let proof =
match proof with
| Terms.Exact t -> Terms.Exact (Subst.apply_subst subst t)
match ty with
| Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
let o = Order.compare_terms l r in
- (vars,Terms.Equation (l, r, ty, o)::literals)
- | _ -> (vars,Terms.Predicate ty::literals)
+ (vars,(Terms.Equation (l, r, ty, o),true)::literals)
+ | _ -> (vars,(Terms.Predicate ty,true)::literals)
in
let varlist = Terms.vars_of_term proofterm in
let (varlist,nlit) = List.fold_left foterm_to_lit (varlist,[]) nlit in