From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 13 Jun 2016 16:27:50 +0000 (+0000)
Subject: does_not_occur documented
X-Git-Tag: make_still_working~564
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e9caa75be87bdbd68d8ca2d7291f623bec6b93aa;p=helm.git

does_not_occur documented
---

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