let proof,goal = status in
let curi, metasenv, _subst, pbo, pty, attrs = proof in
let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
let proof,goal = status in
let curi, metasenv, _subst, pbo, pty, attrs = proof in
let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in