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 (fun u -> not(p u)) !db
  11
  12 let find_coercion f =
  13   List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
  14