]> matita.cs.unibo.it Git - helm.git/commitdiff
removed useless function
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 18 May 2009 15:28:48 +0000 (15:28 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 18 May 2009 15:28:48 +0000 (15:28 +0000)
helm/software/components/ng_kernel/nCicEnvironment.ml
helm/software/components/ng_kernel/nCicEnvironment.mli

index 4d60e5d42948f4729d2d0fef14e951c65985f554..f31c4e9b1ebbc71416ced0dbbc120e4bf60c7448 100644 (file)
@@ -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
index c4fa396cc1d6d493afb4d80644c3b818e0cc2eda..4604bd2fdf2fe4a49537862fe88fc3f53f2ebf9b 100644 (file)
@@ -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