Propagation of changes to grafiteAst.

[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..5f2ac335d3cba50be6fcbf3cf74da070048978c7 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -27,10 +27,11 @@
 
 exception BaseUriNotSetYet
 
+(*
 type tactic = 
  (NotationPt.term, NotationPt.term, 
   NotationPt.term GrafiteAst.reduction, string) 
-   GrafiteAst.tactic
+   GrafiteAst.tactic *)
    
 let singleton msg = function
   | [x], _ -> x
@@ -211,9 +212,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)=
   match cmd with
-   | GrafiteAst.Drop _
    | GrafiteAst.Include _
    | GrafiteAst.Print _
    | GrafiteAst.Set _ as cmd ->