NCic.term -> NCic.term -> NCic.term -> int -> int -> 'status
(* gets the old imperative coercion DB (list format) *)
NCic.term -> NCic.term -> NCic.term -> int -> int -> 'status
(* gets the old imperative coercion DB (list format) *)
NCic.metasenv -> NCic.substitution -> NCic.context ->
(* inferred type, expected type *)
NCic.term -> NCic.term ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
(* inferred type, expected type *)
NCic.term -> NCic.term ->
- (* enriched metasenv, new term, its type, metavriable to
+ (* name, enriched metasenv, new term, its type, metavriable to
(* returns (coercion,arity,arg) *)
val match_coercion:
#status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
context:NCic.context -> NCic.term -> (NCic.term * int * int) option
(* returns (coercion,arity,arg) *)
val match_coercion:
#status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
context:NCic.context -> NCic.term -> (NCic.term * int * int) option