let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in