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