X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=4d66251cebd3307a38c06cecc78b3435575007bc;hb=560db5569f54fba5bded568699a33947f88df3ba;hp=e08908166e179f9fb6d8db6acf92c3604be4e9df;hpb=729e08f5fb86b3ffee460fda4577b024ab5888aa;p=helm.git diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli index e08908166..4d66251ce 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.mli +++ b/matita/components/grafite_parser/grafiteDisambiguate.mli @@ -25,10 +25,11 @@ exception BaseUriNotSetYet +(* type tactic = (NotationPt.term, NotationPt.term, NotationPt.term GrafiteAst.reduction, string) - GrafiteAst.tactic + GrafiteAst.tactic *) val disambiguate_command: LexiconEngine.status as 'status ->