From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 18 May 2009 15:28:48 +0000 (+0000)
Subject: removed useless function
X-Git-Tag: make_still_working~3962
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=95aa33d7e6a77d1e235793f1279ea6428ac522e0;p=helm.git

removed useless function
---

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