X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=6caf5301f200f0f8c667ae5bf534dd5ae8e6c63f;hb=2a59f55f4625ebabb02aefc3cb8c8842040be554;hp=4d66251cebd3307a38c06cecc78b3435575007bc;hpb=560db5569f54fba5bded568699a33947f88df3ba;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli
index 4d66251ce..6caf5301f 100644
--- a/matita/components/grafite_parser/grafiteDisambiguate.mli
+++ b/matita/components/grafite_parser/grafiteDisambiguate.mli
@@ -25,27 +25,15 @@
 
 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
-
 val disambiguate_nterm :
  NCic.term option -> 
- (#NEstatus.status as 'status) ->
+ (#LexiconTypes.status as 'status) ->
  NCic.context -> NCic.metasenv -> NCic.substitution ->
  NotationPt.term Disambiguate.disambiguator_input ->
    NCic.metasenv * NCic.substitution * 'status * NCic.term
 
 val disambiguate_nobj :
- #NEstatus.status as 'status ->
+ #LexiconTypes.status as 'status ->
  ?baseuri:string ->
  (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
   'status * NCic.obj
@@ -56,5 +44,3 @@ type pattern =
 
 val disambiguate_npattern:
   GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
-    
-