(* evals a coercion declaration statement: name t ty (id,src) tgt *)
val eval_ncoercion:
- GrafiteTypes.status as 'status ->
+ #GrafiteTypes.status as 'status ->
string ->
CicNotationPt.term ->
CicNotationPt.term ->
string * CicNotationPt.term ->
- CicNotationPt.term -> 'status * [> `New of 'c list ]
+ CicNotationPt.term -> 'status * [> `New of NUri.uri list ]
(* for records, the term is the projection, already refined, while the
* first integer is the number of left params and the second integer is
* the arity in the `:arity>` syntax *)
-val basic_eval_and_inject_ncoercion_from_t_cpos_arity:
- (GrafiteTypes.status as 'status) ->
- string * NCic.term * int * int -> 'status
+val basic_eval_and_record_ncoercion_from_t_cpos_arity:
+ #GrafiteTypes.status as 'status ->
+ string * NCic.term * int * int -> 'status * [> `New of NUri.uri list ]