+ (* composition of all subst acting on goal *)
+ let res_subst =
+ let rec rsaux ongoal acc =
+ function
+ | [] -> acc (* is the final subst for refl *)
+ | id::tl when ongoal ->
+ let lit,vl,proof = get_literal id in
+ (match proof with
+ | Terms.Exact _ -> rsaux ongoal acc tl
+ | Terms.Step (_, _, _, _, _, s) ->
+ rsaux ongoal (s@acc) tl)
+ | id::tl ->
+ (* subst is the the substitution for refl *)
+ rsaux (id=mp) subst tl
+ in
+ let r = rsaux false [] steps in
+ (* prerr_endline ("res substitution: " ^ Pp.pp_substitution r);
+ prerr_endline ("\n" ^ "subst: " ^ Pp.pp_substitution subst); *)
+ r
+ in