fixed remove_coercion

[helm.git] / helm / ocaml / cic_unification / coercDb.ml

diff --git a/helm/ocaml/cic_unification/coercDb.ml b/helm/ocaml/cic_unification/coercDb.ml
index 149f3a4ab5e781d54589dbf6afb93a25c2f72a1a..6a514b814c95647e1a9b77fc6a06aae868f0b94c 100644 (file)
--- a/helm/ocaml/cic_unification/coercDb.ml
+++ b/helm/ocaml/cic_unification/coercDb.ml
@@ -7,7 +7,7 @@ let add_coercion c =
   db := c :: !db
 
 let remove_coercion p = 
-  db := List.filter p !db
+  db := List.filter (fun u -> not(p u)) !db
 
 let find_coercion f =
   List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)