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

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

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml
index 5f2ac335d3cba50be6fcbf3cf74da070048978c7..8e66319296c7dfe700fe0c14a696a5a383f86313 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -27,12 +27,6 @@
 
 exception BaseUriNotSetYet
 
-(*
-type tactic = 
- (NotationPt.term, NotationPt.term, 
-  NotationPt.term GrafiteAst.reduction, string) 
-   GrafiteAst.tactic *)
-   
 let singleton msg = function
   | [x], _ -> x
   | l, _   ->
@@ -213,7 +207,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
    estatus, cic
 ;;
 
-let disambiguate_command estatus ?baseuri (text,prefix_len,cmd)=
+let disambiguate_command estatus (text,prefix_len,cmd)=
   match cmd with
    | GrafiteAst.Include _
    | GrafiteAst.Print _