exception NotWellFormedTypeOfInductiveConstructor of string
exception WrongRequiredArgument of string
val typecheck : UriManager.uri -> unit
-val type_of: Cic.term -> Cic.term
(* used only in the toplevel *)
(* type_of_aux' metasenv context term *)
-val type_of_aux': (int * Cic.term) list -> Cic.term list -> Cic.term -> Cic.term
+val type_of_aux':
+ Cic.metasenv -> Cic.context -> Cic.term -> Cic.term