fixed last file restricting auto tables

[helm.git] / helm / software / components / tactics / universe.ml

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index a7418461e060603ca6546dc817f9ced288b4a998..780b72daf8e421402e4752a070867ea00044a6db 100644 (file)
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/components/tactics/universe.ml
@@ -31,13 +31,32 @@ module S = Set.Make(Codomain)
 module TI = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(S)
 type universe = TI.t
 
-let empty = TI.empty
+let empty = TI.empty ;;
+
+let iter u f = 
+  TI.iter u 
+   (fun p s -> f p (S.elements s))
 ;;
 
 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