From fea6451862165219503e6e402c70c62f95ec8953 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Jun 2005 11:55:15 +0000 Subject: [PATCH] does_not_occur unexported since it did not have the expected semantics --- helm/ocaml/cic_proof_checking/cicTypeChecker.mli | 5 ----- 1 file changed, 5 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli index a845a332d..5cbda28d6 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli @@ -39,10 +39,5 @@ val type_of_aux': Cic.term -> CicUniv.universe_graph -> Cic.term * CicUniv.universe_graph -(* does_not_occur context lower upper term *) -(* searches for a Cic.Rel i in term with lower < i <= upper *) -val does_not_occur : Cic.context -> int -> int -> Cic.term -> bool - (* typechecks the obj and puts it in the environment *) val typecheck_obj : UriManager.uri -> Cic.obj -> unit - -- 2.39.2