let status, t = disambiguate status ctx ("",0,cand) None in
let status,t = term_of_cic_term status t ctx in
let ty = NCicTypeChecker.typeof subst metasenv ctx t in
let status, t = disambiguate status ctx ("",0,cand) None in
let status,t = term_of_cic_term status t ctx in
let ty = NCicTypeChecker.typeof subst metasenv ctx t in