cicNotation* ==> notation*

[helm.git] / matita / components / grafite_engine / nCicCoercDeclaration.mli

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.mli b/matita/components/grafite_engine/nCicCoercDeclaration.mli
index aee0e9fc390a4463e9681eb46a7d90e76043154a..1c9062fd60807ee2e8c47bbbe2ebdd6b49b1cb40 100644 (file)
--- a/matita/components/grafite_engine/nCicCoercDeclaration.mli
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.mli
@@ -14,10 +14,10 @@
 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 * [> `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