X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Funiverse.ml;h=def2279ca180072e3439506db0e854879452d437;hb=8e76ac2823de8cffc0b5f75b36264f86e3d0b52d;hp=6a0a3156664b6106b965260ac6227a07a1c1fa27;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index 6a0a31566..def2279ca 100644
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/components/tactics/universe.ml
@@ -28,7 +28,7 @@ module Codomain = struct
   let compare = Pervasives.compare 
 end
 module S = Set.Make(Codomain)
-module TI = Discrimination_tree.DiscriminationTreeIndexing(S)
+module TI = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(S)
 type universe = TI.t
 
 let empty = TI.empty
@@ -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
@@ -73,7 +88,7 @@ let rec collapse_head_metas t =
 
 let rec dummies_of_coercions = 
   function
-    | Cic.Appl (c::l) when CoercDb.is_a_coercion' c ->
+    | Cic.Appl (c::l) when CoercDb.is_a_coercion c <> None ->
         Cic.Meta (-1,[])
     | Cic.Appl l -> 
         let l' = List.map dummies_of_coercions l in Cic.Appl l'
@@ -120,7 +135,7 @@ let keys context ty =
     [head true ty; head true (unfold context ty)]
   with ProofEngineTypes.Fail _ -> [head true ty]
 
-let key term = head false term
+let key term = head false term;;
 
 let index_term_and_unfolded_term univ context t ty =
   let key = head true ty in
@@ -162,7 +177,7 @@ let remove univ context term ty =
 
 let remove_uri univ uri =
   let term = CicUtil.term_of_uri uri in
-  let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in
+  let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in
     remove univ [] term ty