]> matita.cs.unibo.it Git - helm.git/commitdiff
fixed remove_coercion
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 9 Jun 2005 11:43:40 +0000 (11:43 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 9 Jun 2005 11:43:40 +0000 (11:43 +0000)
helm/ocaml/cic_unification/coercDb.ml

index 149f3a4ab5e781d54589dbf6afb93a25c2f72a1a..6a514b814c95647e1a9b77fc6a06aae868f0b94c 100644 (file)
@@ -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)