exception TypeCheckerFailure of string
exception AssertFailure of string
-val typecheck : UriManager.uri -> Cic.obj
+val debrujin_constructor : UriManager.uri -> int -> Cic.term -> Cic.term
+
+val typecheck : UriManager.uri -> 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
+
+(* does_not_occur context lower upper term *)
+(* searches for a Cic.Rel i in term with lower < i <= upper *)
+val does_not_occur : Cic.context -> int -> int -> Cic.term -> bool
+
+(* typechecks the obj and puts it in the environment *)
+val typecheck_obj : UriManager.uri -> Cic.obj -> unit
-(* typecheck_mutual_inductive_defs uri (itl,params,indparamsno) *)
-val typecheck_mutual_inductive_defs :
- UriManager.uri -> Cic.inductiveType list * UriManager.uri list * int -> unit