positivity check fixed

[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 f7c3932dc688abf1e5ca3c4acb0308d59b1d4a66..8fb71075589ce85b73efe175942f6f3b3c31c3f7 100644 (file)
--- 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'