X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=7a2e2dda877280596bbefae2bd39cbaa673eda98;hb=b3ce13018a7e6230313124ee2428a91ec5109e51;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..7a2e2dda8 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli @@ -45,7 +45,7 @@ val disambiguate_command: LexiconEngine.status -> baseuri:string option -> 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: