Propagation of changes to grafiteAst.

[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 e08908166e179f9fb6d8db6acf92c3604be4e9df..4d66251cebd3307a38c06cecc78b3435575007bc 100644 (file)
--- 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 ->