X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=b302da1f254227777be6945055ad98ac934c7a2c;hb=f6c887944d48d718f372a57f1609f3d059908aa8;hp=5002e58abca402e7f4691954ca93b7128c6766e5;hpb=13c3708fc59d999727ee214e8ece1f03661a9737;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 5002e58ab..b302da1f2 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -200,7 +200,7 @@ let disambiguate_nterm expty estatus context metasenv subst thing
   let diff, metasenv, subst, cic =
     singleton "first"
       (NCicDisambiguate.disambiguate_term
-        ~rdb:estatus.NEstatus.rstatus
+        ~rdb:estatus.NEstatus.rstatus.NRstatus.refiner_status
         ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases
         ~expty 
         ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases)
@@ -688,7 +688,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
        (try
          (match 
           NCicDisambiguate.disambiguate_obj
-           ~rdb:estatus.NEstatus.rstatus
+           ~rdb:estatus.NEstatus.rstatus.NRstatus.refiner_status
            ~lookup_in_library:nlookup_in_library
            ~description_of_alias:LexiconAst.description_of_alias
            ~mk_choice:ncic_mk_choice
@@ -783,7 +783,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
       ~mk_choice:ncic_mk_choice
       ~mk_implicit
       ~uri:(OCic2NCic.nuri_of_ouri uri)
-      ~rdb:estatus.NEstatus.rstatus
+      ~rdb:estatus.NEstatus.rstatus.NRstatus.refiner_status
       ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases
       ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases) 
       (text,prefix_len,obj)) in