X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.mli;h=98cb72ad773577cd9d2b2e5dc3952dbdf57bc657;hb=13bfd154ade0996d34e7e723398ac7ab76a51717;hp=26dfce3888d7730a0a9433dee93ea696c8958d5d;hpb=48e318104379fb77181c88e83afc5c4814aaba99;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.mli b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
index 26dfce388..98cb72ad7 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
@@ -34,7 +34,8 @@ 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
 
@@ -46,7 +47,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