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