X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fcomponents%2Fgrafite_engine%2FnCicCoercDeclaration.mli;h=9bca1143d3fdb4315be5bd1d5d7f763193cb9ee3;hb=791d52ba005e434be27cca1f8059d9f28da0183b;hp=aee0e9fc390a4463e9681eb46a7d90e76043154a;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.mli b/matita/components/grafite_engine/nCicCoercDeclaration.mli
index aee0e9fc3..9bca1143d 100644
--- a/matita/components/grafite_engine/nCicCoercDeclaration.mli
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.mli
@@ -14,15 +14,15 @@
 val eval_ncoercion: 
    #GrafiteTypes.status as 'status ->
      string ->
-     CicNotationPt.term ->
-     CicNotationPt.term ->
-     string * CicNotationPt.term ->
-     CicNotationPt.term -> 'status * [> `New of NUri.uri list ]
+     NotationPt.term ->
+     NotationPt.term ->
+     string * NotationPt.term ->
+     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 * NCic.term * int * int -> 'status * NUri.uri list