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
+ ?check_exp_named_subst: bool ->
+ UriManager.uri -> int -> Cic.context -> Cic.term -> Cic.term
-val typecheck : UriManager.uri -> Cic.obj * CicUniv.universe_graph
+ (* defaults to true *)
+val typecheck :
+ ?trust:bool -> UriManager.uri -> Cic.obj * CicUniv.universe_graph
(* FUNCTIONS USED ONLY IN THE TOPLEVEL *)
Cic.term -> CicUniv.universe_graph ->
Cic.term * CicUniv.universe_graph
-(* typechecks the obj and puts it in the environment *)
+(* typechecks the obj and puts it in the environment
+ * empty universes are filed with the given uri, thus you should
+ * get the object again after calling this *)
val typecheck_obj : UriManager.uri -> Cic.obj -> unit
(* check_allowed_sort_elimination uri i s1 s2
of the MutCase) *)
val check_allowed_sort_elimination:
UriManager.uri -> int -> Cic.sort -> Cic.sort -> bool
+
+(* does_not_occur ~subst context n nn t
+ checks if the semi-open interval of Rels (n,nn] occurs in t *)
+val does_not_occur:
+ ?subst:Cic.substitution -> Cic.context -> int -> int -> Cic.term -> bool