X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Funiverse.ml;h=def2279ca180072e3439506db0e854879452d437;hb=3a0c71609f757f4ad3aadd234b84486fec97b791;hp=a7418461e060603ca6546dc817f9ced288b4a998;hpb=eaf5880ed69963b3ad37cb1f8a1fd48b2918e58b;p=helm.git

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index a7418461e..def2279ca 100644
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/components/tactics/universe.ml
@@ -38,6 +38,21 @@ let get_candidates univ ty =
   S.elements (TI.retrieve_unifiables univ ty)
 ;;
 
+let in_universe univ ty =
+  let candidates = get_candidates univ ty in
+    List.fold_left 
+      (fun res cand ->
+	 match res with
+	   | Some found -> Some found
+	   | None -> 
+	       let candty,_ = 
+		 CicTypeChecker.type_of_aux' [] [] cand CicUniv.oblivion_ugraph in
+	       let same ,_ = 
+		 CicReduction.are_convertible [] candty ty CicUniv.oblivion_ugraph in
+	       if same then Some cand else None
+      ) None candidates
+;;
+
 let rec unfold context = function
   | Cic.Prod(name,s,t) -> 
       let t' = unfold ((Some (name,Cic.Decl s))::context) t in