From 95aa33d7e6a77d1e235793f1279ea6428ac522e0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 18 May 2009 15:28:48 +0000 Subject: [PATCH] removed useless function --- helm/software/components/ng_kernel/nCicEnvironment.ml | 10 ---------- helm/software/components/ng_kernel/nCicEnvironment.mli | 2 -- 2 files changed, 12 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 4d60e5d42..f31c4e9b1 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -29,16 +29,6 @@ let max l1 l2 = let le_constraints = ref [] (* strict,a,b *) -let resolve_universe u = - HExtlib.list_findopt - (fun (_,a,b) _ -> - prerr_endline (NUri.name_of_uri a); - if NUri.name_of_uri a = u then Some a - else if NUri.name_of_uri b = u then Some b - else None) - !le_constraints -;; - let rec le_path_uri avoid strict a b = (not strict && NUri.eq a b) || List.exists diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index c4fa396cc..4604bd2fd 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -33,8 +33,6 @@ val add_constraint: bool -> NCic.universe -> NCic.universe -> unit val sup : NCic.universe -> NCic.universe option val pp_constraints: unit -> string -val resolve_universe: string -> NUri.uri option - val get_checked_def: NReference.reference -> NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int -- 2.39.2