X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=e08908166e179f9fb6d8db6acf92c3604be4e9df;hb=729e08f5fb86b3ffee460fda4577b024ab5888aa;hp=4392de8702cd00628dc7faa2072f557b269a5c26;hpb=d284dd23d0e12a62a001d3473eadf4942d12ffaa;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli
index 4392de870..e08908166 100644
--- a/matita/components/grafite_parser/grafiteDisambiguate.mli
+++ b/matita/components/grafite_parser/grafiteDisambiguate.mli
@@ -33,8 +33,8 @@ type tactic =
 val disambiguate_command: 
  LexiconEngine.status as 'status ->
  ?baseuri:string ->
- ((NotationPt.term,NotationPt.term NotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
-  'status * (Cic.term,Cic.obj) GrafiteAst.command
+ GrafiteAst.command Disambiguate.disambiguator_input ->
+  'status * GrafiteAst.command
 
 val disambiguate_nterm :
  NCic.term option ->