]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_parser/grafiteDisambiguate.ml
FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:
[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml
index 5002e58abca402e7f4691954ca93b7128c6766e5..b302da1f254227777be6945055ad98ac934c7a2c 100644 (file)
@@ -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