Initial implementation of statuses using objects in place of nested records.

[helm.git] / helm / software / components / ng_disambiguation / nCicDisambiguate.ml

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 108c845c69670eb8b6e5aa44c129d357da1e6ed1..5fa3b81887b9b7f17ff4fe52a23fb4ee6fb1b6da 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -47,9 +47,8 @@ let refine_term
     in
     let metasenv, subst, term, _ = 
       NCicRefiner.typeof 
-        { rdb with NRstatus.coerc_db = 
-           if use_coercions then rdb.NRstatus.coerc_db 
-           else NCicCoercion.empty_db }
+        (rdb#set_coerc_db 
+          (if use_coercions then rdb#coerc_db else NCicCoercion.empty_db))
         metasenv subst context term expty ~localise 
     in
      Disambiguate.Ok (term, metasenv, subst, ())
@@ -79,9 +78,9 @@ let refine_obj
   try
     let obj =
       NCicRefiner.typeof_obj
-        { rdb with NRstatus.coerc_db = 
-           if use_coercions then rdb.NRstatus.coerc_db 
-           else NCicCoercion.empty_db }
+        (rdb#set_coerc_db
+           (if use_coercions then rdb#coerc_db 
+            else NCicCoercion.empty_db))
         obj ~localise 
     in
       Disambiguate.Ok (obj, [], [], ())