(* type_of_aux' metasenv context term *)
(* refines [term] and returns the refined form of [term], *)
-(* its type, the computed substitution and the new metasenv. *)
+(* its type the new metasenv. *)
val type_of_aux':
Cic.metasenv -> Cic.context -> Cic.term ->
Cic.term * Cic.term * Cic.metasenv