~start:(fun ~status:(proof,goal as status) ->
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal)
~start:(fun ~status:(proof,goal as status) ->
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal)