let aux ((proof,goal) as status) =
let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in
let _,context,gty = CicUtil.lookup_meta goal metasenv in
let aux ((proof,goal) as status) =
let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in
let _,context,gty = CicUtil.lookup_meta goal metasenv in