X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaEngine.mli;h=945e7f348d888dea000de4438690e2f31044f0e3;hb=560db5569f54fba5bded568699a33947f88df3ba;hp=070a7a48f92b4bf799b5b3e1b170e73f80115e14;hpb=729e08f5fb86b3ffee460fda4577b024ab5888aa;p=helm.git

diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli
index 070a7a48f..945e7f348 100644
--- a/matita/matita/matitaEngine.mli
+++ b/matita/matita/matitaEngine.mli
@@ -27,9 +27,7 @@ val eval_ast :
   ?do_heavy_checks:bool ->
   GrafiteTypes.status ->
   string * int *
-  ((NotationPt.term, NotationPt.term,
-   NotationPt.term GrafiteAst.reduction, NotationPt.term NotationPt.obj, string)
-   GrafiteAst.statement) ->
+  GrafiteAst.statement ->
   (GrafiteTypes.status *
    (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list
 
@@ -49,9 +47,6 @@ val eval_from_stream :
   ?watch_statuses:(GrafiteTypes.status -> unit) ->
   GrafiteTypes.status ->
   Ulexing.lexbuf ->
-  (GrafiteTypes.status ->
-   (NotationPt.term, NotationPt.term,
-    NotationPt.term GrafiteAst.reduction, NotationPt.term NotationPt.obj, string)
-   GrafiteAst.statement -> unit) ->
+  (GrafiteTypes.status -> GrafiteAst.statement -> unit) ->
   (GrafiteTypes.status *
    (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list