How do I obtain the type of term? To type a term of the calculus of the construction, you need to use Mach.type_of. The arguments to provide to this function usually are Evd.mt_evd() and (initial_sign()), if all free identifiers in the term are declared in the global environment. If you have some free identifiers, for which you know the expected type, you can add them in the signature given by (intial_sign()), using Mach.fexecute_type to create a type_judgement and add_sign to add a binding in the signature.
This does not work if there are "unbound" de Bruijn indices.