- hExtlib: added debugging information for split_nth

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.mli

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.mli b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
index e9419171e906140ea1c9685ff56e7deba12858d9..a3361fc7be609f6c860cd5788de5662bb59fd148 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
@@ -34,9 +34,12 @@ exception AssertFailure of string Lazy.t
    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 *)
 
@@ -46,7 +49,9 @@ val type_of_aux':
   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
@@ -59,3 +64,8 @@ val typecheck_obj : UriManager.uri -> Cic.obj -> unit
         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