X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FnCicCoercDeclaration.mli;h=aee0e9fc390a4463e9681eb46a7d90e76043154a;hb=4edcf284d13d4f0f945234482fda852e7b7180c4;hp=66698156857b6a51c1f8d91a445c8453cb906c5c;hpb=889815067d64e081eb90ea1a792890c2ad4e511c;p=helm.git

diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.mli b/helm/software/components/grafite_engine/nCicCoercDeclaration.mli
index 666981568..aee0e9fc3 100644
--- a/helm/software/components/grafite_engine/nCicCoercDeclaration.mli
+++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.mli
@@ -12,17 +12,17 @@
 
 (* 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 ]