cicNotation* ==> notation*

[helm.git] / matita / matita / matitaEngine.mli

diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli
index 92b2d8e1c1eda89b57cc1a865b2db1633db99dec..070a7a48f92b4bf799b5b3e1b170e73f80115e14 100644 (file)
--- a/matita/matita/matitaEngine.mli
+++ b/matita/matita/matitaEngine.mli
@@ -27,8 +27,8 @@ val eval_ast :
   ?do_heavy_checks:bool ->
   GrafiteTypes.status ->
   string * int *
-  ((CicNotationPt.term, CicNotationPt.term,
-   CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string)
+  ((NotationPt.term, NotationPt.term,
+   NotationPt.term GrafiteAst.reduction, NotationPt.term NotationPt.obj, string)
    GrafiteAst.statement) ->
   (GrafiteTypes.status *
    (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list
@@ -50,8 +50,8 @@ val eval_from_stream :
   GrafiteTypes.status ->
   Ulexing.lexbuf ->
   (GrafiteTypes.status ->
-   (CicNotationPt.term, CicNotationPt.term,
-    CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string)
+   (NotationPt.term, NotationPt.term,
+    NotationPt.term GrafiteAst.reduction, NotationPt.term NotationPt.obj, string)
    GrafiteAst.statement -> unit) ->
   (GrafiteTypes.status *
    (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list