exception TypeCheckerFailure of string
exception AssertFailure of string
-val typecheck : UriManager.uri -> unit
+val typecheck :
+ UriManager.uri -> CicUniv.universe_graph -> Cic.obj * CicUniv.universe_graph
(* FUNCTIONS USED ONLY IN THE TOPLEVEL *)
(* 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 -> CicUniv.universe_graph ->
+ Cic.term * CicUniv.universe_graph
+
(* typecheck_mutual_inductive_defs uri (itl,params,indparamsno) *)
val typecheck_mutual_inductive_defs :
- UriManager.uri -> Cic.inductiveType list * UriManager.uri list * int -> unit
+ UriManager.uri -> Cic.inductiveType list * UriManager.uri list * int ->
+ CicUniv.universe_graph -> CicUniv.universe_graph