X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=5fa3b81887b9b7f17ff4fe52a23fb4ee6fb1b6da;hb=ee7855524284ea3a282c68f22ffa36e535a11810;hp=108c845c69670eb8b6e5aa44c129d357da1e6ed1;hpb=dcdbb979433a61e2ef2842d96604098728824416;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 108c845c6..5fa3b8188 100644
--- 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, [], [], ())