X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=582ab11ec8afc0050e7058e256379e29e42ed58c;hb=1238c59b078908f3923aa2e03adee7fe7a291027;hp=b04aa3cde54530fea0e1c1419a9cda97aa8c9bb8;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
index b04aa3cde..582ab11ec 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -25,24 +25,32 @@
 
 exception BaseUriNotSetYet
 
+type tactic = 
+ (CicNotationPt.term, CicNotationPt.term, 
+  CicNotationPt.term GrafiteAst.reduction, string) 
+   GrafiteAst.tactic
+
+type lazy_tactic = 
+  (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) 
+    GrafiteAst.tactic
+
 val disambiguate_tactic:
  LexiconEngine.status ref ->
  Cic.context ->
  Cic.metasenv ->
- (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string) GrafiteAst.tactic ->
-  Cic.metasenv *
-   (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic
+ tactic Disambiguate.disambiguator_input ->
+  Cic.metasenv * lazy_tactic
 
 val disambiguate_command: 
  LexiconEngine.status ->
  baseuri:string option ->
  Cic.metasenv ->
-  CicNotationPt.obj GrafiteAst.command ->
+ (CicNotationPt.obj GrafiteAst.command) Disambiguate.disambiguator_input ->
   LexiconEngine.status * Cic.metasenv * Cic.obj GrafiteAst.command
 
 val disambiguate_macro:
  LexiconEngine.status ref ->
  Cic.metasenv ->
  Cic.context ->
-  CicNotationPt.term GrafiteAst.macro ->
+ (CicNotationPt.term GrafiteAst.macro) Disambiguate.disambiguator_input ->
   Cic.metasenv * Cic.term GrafiteAst.macro