From 48e318104379fb77181c88e83afc5c4814aaba99 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 10 Apr 2008 18:09:01 +0000 Subject: [PATCH 1/1] does_not_occur exported to be used in oCic2NCic --- .../components/cic_proof_checking/cicTypeChecker.mli | 5 +++++ 1 file changed, 5 insertions(+) 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 -- 2.39.2