let prova_tac =
let apply_T_tac ~status:((proof,goal) as status) =
let curi,metasenv,pbo,pty = proof in
- let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,gty = CicUtil.lookup_meta goal metasenv in
let rel =
let rec find n =
function