let status,t = term_of_cic_term status t ctx in
let _,_,metasenv,subst,_ = status#obj in
let ty = NCicTypeChecker.typeof subst metasenv ctx t in
let status,t = term_of_cic_term status t ctx in
let _,_,metasenv,subst,_ = status#obj in
let ty = NCicTypeChecker.typeof subst metasenv ctx t in