X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.mli;h=a3361fc7be609f6c860cd5788de5662bb59fd148;hb=bca340f9c590e6530f8346fddd61c9fa0ae7f411;hp=e1c113ef335609f9460efb981910518629f792ad;hpb=97b18234921aec71a8b89ec2c1b058e12e5e043c;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.mli b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
index e1c113ef3..a3361fc7b 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
@@ -37,7 +37,9 @@ val debrujin_constructor :
  ?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 *)
 
@@ -47,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