X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=11fcbab1dd785294af545ba9745ddb5135d53276;hb=8bc5bc0e8375a85736f6a5df317d129d5efa8de4;hp=b8814d4d8a7b133c3b87f4c0a0a73c80ed55c637;hpb=e898ca2563cc4dfbd328efc7aa3a4ff86feaec92;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
index b8814d4d8..11fcbab1d 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -42,11 +42,11 @@ val disambiguate_tactic:
   Cic.metasenv * lazy_tactic
 
 val disambiguate_command: 
- LexiconEngine.status ->
+ NEstatus.extra_status ->
  ?baseuri:string ->
  Cic.metasenv ->
  ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
-  LexiconEngine.status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
+  NEstatus.extra_status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
 
 val disambiguate_macro:
  LexiconEngine.status ref ->
@@ -56,10 +56,17 @@ val disambiguate_macro:
   Cic.metasenv * (Cic.term,Cic.lazy_term) GrafiteAst.macro
 
 val disambiguate_nterm :
- NCic.term option -> LexiconEngine.status ->
+ NCic.term option -> 
+ NEstatus.extra_status ->
  NCic.context -> NCic.metasenv -> NCic.substitution ->
  CicNotationPt.term Disambiguate.disambiguator_input ->
-   NCic.metasenv * NCic.substitution * LexiconEngine.status * NCic.term
+   NCic.metasenv * NCic.substitution * NEstatus.extra_status * NCic.term
+
+val disambiguate_nobj :
+ NEstatus.extra_status ->
+ ?baseuri:string ->
+ (CicNotationPt.term CicNotationPt.obj) Disambiguate.disambiguator_input ->
+  NEstatus.extra_status * NCic.obj
 
 type pattern = 
   CicNotationPt.term Disambiguate.disambiguator_input option *