- 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 07e502822f5d0f4ceae76c6cff36d34b5f859e2d..8e66319296c7dfe700fe0c14a696a5a383f86313 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -27,11 +27,6 @@
 
 exception BaseUriNotSetYet
 
-type tactic = 
- (NotationPt.term, NotationPt.term, 
-  NotationPt.term GrafiteAst.reduction, string) 
-   GrafiteAst.tactic
-   
 let singleton msg = function
   | [x], _ -> x
   | l, _   ->
@@ -211,9 +206,9 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
   let estatus = LexiconEngine.set_proof_aliases estatus diff in
    estatus, cic
 ;;
-let disambiguate_command estatus ?baseuri (text,prefix_len,cmd)=
+
+let disambiguate_command estatus (text,prefix_len,cmd)=
   match cmd with
-   | GrafiteAst.Drop _
    | GrafiteAst.Include _
    | GrafiteAst.Print _
    | GrafiteAst.Set _ as cmd ->