(* type_of_aux' metasenv context term *)
val type_of_aux':
- Cic.metasenv -> Cic.context -> Cic.term -> Cic.term
+ ?subst:Cic.substitution -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term
(* typecheck_mutual_inductive_defs uri (itl,params,indparamsno) *)
val typecheck_mutual_inductive_defs :