added support for coercions

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

diff --git a/helm/ocaml/cic_unification/coercDb.ml b/helm/ocaml/cic_unification/coercDb.ml
new file mode 100644 (file)
index 0000000..149f3a4
--- /dev/null
+++ b/helm/ocaml/cic_unification/coercDb.ml
@@ -0,0 +1,14 @@
+let db = ref []
+
+let to_list () =
+  !db
+
+let add_coercion c =
+  db := c :: !db
+
+let remove_coercion p = 
+  db := List.filter p !db
+
+let find_coercion f =
+  List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
+