let gty = get_goalty status goal in
let n,h,metasenv,subst,o = status#obj in
let status,t = term_of_cic_term status gty (ctx_of gty) in
let gty = get_goalty status goal in
let n,h,metasenv,subst,o = status#obj in
let status,t = term_of_cic_term status gty (ctx_of gty) in