X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FnCicCoercDeclaration.mli;h=66e3a561b33ca5c65dc1f69b0ef6f26f5b7b80aa;hb=dd627e471392375ca7b6dad78a931a8682e06dbe;hp=9bca1143d3fdb4315be5bd1d5d7f763193cb9ee3;hpb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;p=helm.git diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.mli b/matita/components/grafite_engine/nCicCoercDeclaration.mli index 9bca1143d..66e3a561b 100644 --- a/matita/components/grafite_engine/nCicCoercDeclaration.mli +++ b/matita/components/grafite_engine/nCicCoercDeclaration.mli @@ -10,10 +10,11 @@ V_______________________________________________________________ *) -(* evals a coercion declaration statement: name t ty (id,src) tgt *) +(* evals a coercion declaration statement: name compose t ty (id,src) tgt *) val eval_ncoercion: #GrafiteTypes.status as 'status -> string -> + bool -> NotationPt.term -> NotationPt.term -> string * NotationPt.term -> @@ -24,5 +25,5 @@ val eval_ncoercion: * the arity in the `:arity>` syntax *) val basic_eval_and_record_ncoercion_from_t_cpos_arity: #GrafiteTypes.status as 'status -> - string * NCic.term * int * int -> 'status * NUri.uri list + string * bool * NCic.term * int * int -> 'status * NUri.uri list