let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
let term = C.Sort C.Set in
let letout_tac (proof, goal) =
let curi, metasenv, pbo, pty = proof in
let metano, context, ty = CicUtil.lookup_meta goal metasenv in
let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
let term = C.Sort C.Set in
let letout_tac (proof, goal) =
let curi, metasenv, pbo, pty = proof in
let metano, context, ty = CicUtil.lookup_meta goal metasenv in