]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/grafite_engine/nCicCoercDeclaration.mli
urimanager removed
[helm.git] / matita / components / grafite_engine / nCicCoercDeclaration.mli
index 1c9062fd60807ee2e8c47bbbe2ebdd6b49b1cb40..9bca1143d3fdb4315be5bd1d5d7f763193cb9ee3 100644 (file)
@@ -17,12 +17,12 @@ val eval_ncoercion:
      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 * NCic.term * int * int -> 'status * NUri.uri list