X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FnCicCoercDeclaration.mli;h=66e3a561b33ca5c65dc1f69b0ef6f26f5b7b80aa;hb=e28ddccd4096c80b2090ca78af00e2590f629b71;hp=1c9062fd60807ee2e8c47bbbe2ebdd6b49b1cb40;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.mli b/matita/components/grafite_engine/nCicCoercDeclaration.mli
index 1c9062fd6..66e3a561b 100644
--- a/matita/components/grafite_engine/nCicCoercDeclaration.mli
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.mli
@@ -10,19 +10,20 @@
       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 ->
-     NotationPt.term -> 'status * [> `New of NUri.uri list ]
+     NotationPt.term -> 'status * 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_record_ncoercion_from_t_cpos_arity: 
    #GrafiteTypes.status as 'status ->
-     string * NCic.term * int * int -> 'status * [> `New of NUri.uri list ]
+     string * bool * NCic.term * int * int -> 'status * NUri.uri list