- bug fixed (introduced by last commit from Andrea in MatitaEngine):

[helm.git] / matita / components / grafite_parser / grafiteDisambiguate.mli

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli
index 4d66251cebd3307a38c06cecc78b3435575007bc..2de3a1b6d7ec4880a4014a73dd6f66453dbb2d23 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.mli
+++ b/matita/components/grafite_parser/grafiteDisambiguate.mli
@@ -25,15 +25,8 @@
 
 exception BaseUriNotSetYet
 
-(*
-type tactic = 
- (NotationPt.term, NotationPt.term, 
-  NotationPt.term GrafiteAst.reduction, string) 
-   GrafiteAst.tactic *)
-
 val disambiguate_command: 
  LexiconEngine.status as 'status ->
- ?baseuri:string ->
  GrafiteAst.command Disambiguate.disambiguator_input ->
   'status * GrafiteAst.command