exception TypeCheckerFailure of string Lazy.t
exception AssertFailure of string Lazy.t
-val debrujin_constructor : UriManager.uri -> int -> Cic.term -> Cic.term
+(* this function is exported to be used also by the refiner;
+ the callback function (defaul value: ignore) is invoked on each
+ processed subterm; its first argument is the undebrujined term (the
+ input); its second argument the corresponding debrujined term (the
+ output). The callback is used to relocalize the error messages *)
+val debrujin_constructor :
+ ?cb:(Cic.term -> Cic.term -> unit) ->
+ UriManager.uri -> int -> Cic.term -> Cic.term
val typecheck : UriManager.uri -> Cic.obj * CicUniv.universe_graph