X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=379b65c1e17d39ae5dc0736a2fbf19c448ef1ef6;hb=7a7af8e1ed42aa440476975ec918d38f0c3d13c9;hp=21836853f05aec0108b30c39879a837168abdedb;hpb=a58d25c192ff13ecee2cb92f07ee6f1cbe5219b5;p=helm.git

diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.mli b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli
index 21836853f..379b65c1e 100644
--- a/helm/ocaml/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli
@@ -32,5 +32,6 @@ val disambiguate_tactic:
 
 val disambiguate_command: 
  GrafiteTypes.status ->
-  (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command ->
-  GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command
+  CicNotationPt.obj GrafiteAst.command ->
+  GrafiteTypes.status * Cic.obj GrafiteAst.command
+