X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=1543387ee355af220bd16cef49974519505dfe82;hb=0080faad4e730c227b6bbb2549407b23703b477a;hp=f78507042e18d174c6a66f357d018cd99a2fe2f0;hpb=7b4d519aefac94afb371a7e4da94779b40bf8608;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
index f78507042..1543387ee 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -37,20 +37,20 @@ type lazy_tactic =
 val disambiguate_tactic:
  LexiconEngine.status ref ->
  Cic.context ->
- Cic.metasenv ->
+ Cic.metasenv -> int option ->
  tactic Disambiguate.disambiguator_input ->
   Cic.metasenv * lazy_tactic
 
 val disambiguate_command: 
  LexiconEngine.status ->
- baseuri:string option ->
+ ?baseuri:string ->
  Cic.metasenv ->
- ((CicNotationPt.term,CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
+ ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
   LexiconEngine.status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
 
 val disambiguate_macro:
  LexiconEngine.status ref ->
  Cic.metasenv ->
  Cic.context ->
- (CicNotationPt.term GrafiteAst.macro) Disambiguate.disambiguator_input ->
-  Cic.metasenv * Cic.term GrafiteAst.macro
+ ((CicNotationPt.term,CicNotationPt.term) GrafiteAst.macro) Disambiguate.disambiguator_input ->
+  Cic.metasenv * (Cic.term,Cic.lazy_term) GrafiteAst.macro