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

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index f7c3932dc..a7418461e 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
@@ -73,7 +73,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'