From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 10 Apr 2008 18:09:01 +0000 (+0000)
Subject: does_not_occur exported to be used in oCic2NCic
X-Git-Tag: make_still_working~5371
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=48e318104379fb77181c88e83afc5c4814aaba99;p=helm.git

does_not_occur exported to be used in oCic2NCic
---

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.mli b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
index e9419171e..26dfce388 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
@@ -59,3 +59,8 @@ val typecheck_obj : UriManager.uri -> Cic.obj -> unit
         of the MutCase) *)
 val check_allowed_sort_elimination:
  UriManager.uri -> int -> Cic.sort -> Cic.sort -> bool
+
+(* does_not_occur ~subst context n nn t
+   checks if the semi-open interval of Rels (n,nn] occurs in t *)
+val does_not_occur:
+ ?subst:Cic.substitution -> Cic.context -> int -> int -> Cic.term -> bool