-(*
- let morphism, l, r =
- let p =
- if (ongoal=true) = (dir=Terms.Left2Right) then
- p_id2
- else sym p_id2 in
- let id1_ty = ty_of id1 seen in
- let id2_ty,l,r =
- match ty_of id2 seen with
- | Terms.Node [ _; t; l; r ] ->
- extract amount vl (Subst.apply_subst subst t),
- extract amount vl (Subst.apply_subst subst l),
- extract amount vl (Subst.apply_subst subst r)
- | _ -> assert false
- in
- (*prerr_endline "mk_predicate :";
- if ongoal then prerr_endline "ongoal=true"
- else prerr_endline "ongoal=false";
- prerr_endline ("id=" ^ string_of_int id);
- prerr_endline ("id1=" ^ string_of_int id1);
- prerr_endline ("id2=" ^ string_of_int id2);
- prerr_endline ("Positions :" ^
- (String.concat ", "
- (List.map string_of_int pos)));*)
- mk_morphism
- p amount (Subst.apply_subst subst id1_ty) pos vl,
- l,r
- in
- let rewrite_step = iff1 morphism p_id1
- in
-*)