]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_parser/grafiteDisambiguate.ml
1) NCicLibrary (which is untrusted) moved after NCicUntrusted.
[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml
index 5002e58abca402e7f4691954ca93b7128c6766e5..64c4c8ebe9e2d84043224b891aee6ca861575804 100644 (file)
@@ -170,7 +170,7 @@ let nlookup_in_library
          ) references @
         lookup_in_library interactive_user_uri_choice input_or_locate_uri item
       with
-       NCicLibrary.ObjectNotFound _ ->
+       NCicEnvironment.ObjectNotFound _ ->
         lookup_in_library interactive_user_uri_choice input_or_locate_uri item)
   | _ -> lookup_in_library interactive_user_uri_choice input_or_locate_uri item 
 ;;
@@ -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