does_not_occur documented

diff --git a/matita/components/ng_kernel/nCicTypeChecker.mli b/matita/components/ng_kernel/nCicTypeChecker.mli
index 6ca329fbff1c9f97e81dedec445080fae5db5d5b..34abacfde29654e602c12262fc2b046ef30dec65 100644 (file)
--- 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