Large commit:

[helm.git] / matita / components / grafite_engine / nCicCoercDeclaration.ml

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml
index e370975d798fabd79384c536d357d55381c1e501..e204422e35e973b3918b9b16cb471b4fe31ba5f4 100644 (file)
--- a/matita/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml
@@ -301,8 +301,7 @@ let record_ncoercion =
 
 let basic_eval_and_record_ncoercion infos status =
  let uris, cinfos, status = basic_eval_ncoercion infos status in
- let dump = record_ncoercion (infos::cinfos) :: status#dump in
-  status#set_dump dump, uris
+  NCicLibrary.dump_obj status (record_ncoercion (infos::cinfos)), uris
 ;;
 
 let basic_eval_and_record_ncoercion_from_t_cpos_arity