X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Funiverse.ml;h=8fb71075589ce85b73efe175942f6f3b3c31c3f7;hb=1c2cadee5d666f0e31085a4ff358d667379c4f25;hp=c4e439efe34ca8ffa579b4e94a95e7ebd0066a70;hpb=d030f02fa8a708cd663ffd0c5783770906b9b21a;p=helm.git

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index c4e439efe..8fb710755 100644
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/components/tactics/universe.ml
@@ -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'
@@ -162,7 +162,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