X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FdoubleTypeInference.mli;h=d7d06ae42346f96eb3cb89ab0128597b7d0e4d5e;hb=2f73b29c0ae7e4f0fa77934db55ebf811638fce3;hp=aa151988b233875ab4721aa3106b2189a73bd778;hpb=487bad7921f803801c4df83bf75c237927321fb1;p=helm.git

diff --git a/helm/gTopLevel/doubleTypeInference.mli b/helm/gTopLevel/doubleTypeInference.mli
index aa151988b..d7d06ae42 100644
--- a/helm/gTopLevel/doubleTypeInference.mli
+++ b/helm/gTopLevel/doubleTypeInference.mli
@@ -17,3 +17,9 @@ module CicHash :
 
 val double_type_of :
  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types CicHash.t
+
+(** Auxiliary functions **)
+
+(* does_not_occur n te                              *)
+(* returns [true] if [Rel n] does not occur in [te] *)
+val does_not_occur : int -> Cic.term -> bool