X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=f13fc418cd381ae6f20d36fe96fbb0f53887b1cf;hb=e085135177f7b3b74b410d47a4f3bca1784b60b1;hp=b8814d4d8a7b133c3b87f4c0a0a73c80ed55c637;hpb=585469505faa97c21687128490828a1aabee94ee;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
index b8814d4d8..f13fc418c 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -61,6 +61,11 @@ val disambiguate_nterm :
  CicNotationPt.term Disambiguate.disambiguator_input ->
    NCic.metasenv * NCic.substitution * LexiconEngine.status * NCic.term
 
+val disambiguate_nobj :
+ LexiconEngine.status -> ?baseuri:string ->
+ (CicNotationPt.term CicNotationPt.obj) Disambiguate.disambiguator_input ->
+  LexiconEngine.status * NCic.obj
+
 type pattern = 
   CicNotationPt.term Disambiguate.disambiguator_input option * 
   (string * NCic.term) list * NCic.term option