val index_hint:
db -> NCic.context -> NCic.term -> NCic.term -> int -> db
- (* gets the old imperative coercion DB *)
-val db : unit -> db
-val add_user_provided_hint : Cic.term -> int -> unit
+val add_user_provided_hint : db -> NCic.term -> int -> db
val empty_db : db