application arguments are compared with test_eq_only=true

[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 e1c113ef335609f9460efb981910518629f792ad..98cb72ad773577cd9d2b2e5dc3952dbdf57bc657 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
@@ -47,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