X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=798fa75f528ed734f5e85db3ae9330156582ca29;hb=ac31c84bb9bcf327554976d4296d787853fc8db5;hp=7a2e2dda877280596bbefae2bd39cbaa673eda98;hpb=4609a07e2fe4343d94832fcaf0936223f83ba71c;p=helm.git diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli index 7a2e2dda8..798fa75f5 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli @@ -43,7 +43,7 @@ val disambiguate_tactic: val disambiguate_command: LexiconEngine.status -> - baseuri:string option -> + ?baseuri:string -> Cic.metasenv -> ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input -> LexiconEngine.status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command