type db
-val set_convert_term:
- (UriManager.uri -> Cic.term -> NCic.term * NCic.obj list) -> unit
-
class type g_status =
object
inherit NCicUnifHint.g_status
method coerc_db: db
end
-class status :
+class virtual status :
object ('self)
- inherit NCicUnifHint.status
inherit g_status
- method coerc_db: db
+ inherit NCicUnifHint.status
method set_coerc_db: db -> 'self
method set_coercion_status: #g_status -> 'self
end
#status as 'status -> string ->
NCic.term -> NCic.term -> NCic.term -> int -> int -> 'status
+(* NOTE: the name of the coercion is used to sort coercions, thus
+ * two coercions matching the same number of symbols are sorted
+ * according to their name *)
val look_for_coercion:
#status ->
NCic.metasenv -> NCic.substitution -> NCic.context ->