~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_
~start:(fun ~status:(proof,goal as status) ->
let curi,metasenv,pbo,pty = proof in
~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_
~start:(fun ~status:(proof,goal as status) ->
let curi,metasenv,pbo,pty = proof in