let destruct status =
let (proof, goal) = status in
let _,metasenv,_subst, _,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let destruct status =
let (proof, goal) = status in
let _,metasenv,_subst, _,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in