X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=439a817d3f5f127318dfc789e689fb6174edbf87;hb=0fde70bd19b8fdfa72b807b9713a02ad1bd91b5b;hp=e17769ec98e2be2d0da4148490597dc26577581f;hpb=f61ffe97078aab1e47ee1b7f212e707b0412e77e;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli
index e17769ec9..439a817d3 100644
--- a/matita/components/grafite_parser/grafiteDisambiguate.mli
+++ b/matita/components/grafite_parser/grafiteDisambiguate.mli
@@ -37,9 +37,8 @@ type lazy_tactic =
 val disambiguate_command: 
  LexiconEngine.status as 'status ->
  ?baseuri:string ->
- Cic.metasenv ->
  ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
-  'status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
+  'status * (Cic.term,Cic.obj) GrafiteAst.command
 
 val disambiguate_nterm :
  NCic.term option ->