X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.mli;h=34abacfde29654e602c12262fc2b046ef30dec65;hb=f00a612006ac05f49a42ab507a95d3298bc1457a;hp=6ca329fbff1c9f97e81dedec445080fae5db5d5b;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

diff --git a/matita/components/ng_kernel/nCicTypeChecker.mli b/matita/components/ng_kernel/nCicTypeChecker.mli
index 6ca329fbf..34abacfde 100644
--- a/matita/components/ng_kernel/nCicTypeChecker.mli
+++ b/matita/components/ng_kernel/nCicTypeChecker.mli
@@ -64,6 +64,10 @@ val are_all_occurrences_positive:
  #NCic.status -> subst:NCic.substitution -> NCic.context -> NUri.uri -> int ->
   int -> int -> int -> NCic.term -> bool
 
+(* does_not_occur ... n nn t
+ * detects the Rels m of t in the range n < m <= nn
+ * recursively delta-expanding the Rels m of t in the range 0 < m <= n
+ *)
 val does_not_occur :
  #NCic.status -> subst:NCic.substitution -> NCic.context -> int -> int ->
   NCic.term -> bool