let n,h,metasenv,subst,o = status#obj in
let gname, ctx, gty = List.assoc g metasenv in
(* let ggty = mk_cic_term context gty in *)
let n,h,metasenv,subst,o = status#obj in
let gname, ctx, gty = List.assoc g metasenv in
(* let ggty = mk_cic_term context gty in *)