match goallist with
[] -> warn ("Tacticals.solve_tactics: " ^ descr ^ " solved the goal!!!");
(* questo significa che non ci sono piu' goal, o che current_tactic non ne ha aperti di nuovi? (la 2a!) ##### *)
(* nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *)
(proof, goallist)
| _ -> warn ("Tacticals.solve_tactics: try the next tactic");
match goallist with
[] -> warn ("Tacticals.solve_tactics: " ^ descr ^ " solved the goal!!!");
(* questo significa che non ci sono piu' goal, o che current_tactic non ne ha aperti di nuovi? (la 2a!) ##### *)
(* nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *)
(proof, goallist)
| _ -> warn ("Tacticals.solve_tactics: try the next tactic");