]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_unification/coercDb.ml
added support for coercions
[helm.git] / helm / ocaml / cic_unification / coercDb.ml
1 let db = ref []
2
3 let to_list () =
4   !db
5
6 let add_coercion c =
7   db := c :: !db
8
9 let remove_coercion p = 
10   db := List.filter p !db
11
12 let find_coercion f =
13   List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
14