-print_endline ("-- SUBST " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t p (snd sub));\r
- let p = {p with stepped=(fst sub)::p.stepped} in\r
- let conv = subst sub p.conv in\r
- let div = subst sub p.div in\r
- let p = {p with div; conv} in\r
- (* print_endline ("after sub: \n" ^ string_of_problem p); *)\r
- {p with sigma=sub::p.sigma}\r
+print_endline ("-- SUBST " ^ string_of_t (V (fst sub)) ^ " |-> " ^ string_of_t (snd sub));\r
+ {p with\r
+ div=subst sub p.div;\r
+ conv=subst sub p.conv;\r
+ stepped=(fst sub)::p.stepped;\r
+ sigma=sub::p.sigma}\r