+let add_coercion (src,tgt,u) =
+ let f s t = eq_carr s src && eq_carr t tgt in
+ let where = List.filter (fun (s,t,_) -> f s t) !db in
+ let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in
+ match where with
+ | [] -> db := (src,tgt,[u]) :: !db
+ | (src,tgt,l)::tl ->
+ assert (tl = []); (* not sure, this may be a feature *)
+ db := (src,tgt,u::l)::tl @ rest
+;;
+