exception TypeCheckerFailure of string
exception AssertFailure of string
-val typecheck :
- UriManager.uri -> CicUniv.universe_graph -> Cic.obj * CicUniv.universe_graph
+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 *)
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 ->
- CicUniv.universe_graph -> CicUniv.universe_graph
+(* typechecks the obj and puts it in the environment *)
+val typecheck_obj : UriManager.uri -> Cic.obj -> unit