X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FnCicCoercDeclaration.ml;h=e204422e35e973b3918b9b16cb471b4fe31ba5f4;hb=7ad16d18416a08382d62747fce4a0ac18ee557e0;hp=4522a0a1a917855a8aed045d35b1eaa52d753e94;hpb=d4f2d4c1a4784f84aa27e1bb96b8b377a6553c65;p=helm.git

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml
index 4522a0a1a..e204422e3 100644
--- a/matita/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml
@@ -289,17 +289,19 @@ let record_ncoercion =
    basic_index_ncoercion (name,t,s,d,p,a)
  in
  let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term
-  ~refresh_uri_in_reference
+  ~refresh_uri_in_reference ~alias_only status
  =
-   List.fold_right (aux ~refresh_uri_in_term) l
+  if not alias_only then
+   List.fold_right (aux ~refresh_uri_in_term) l status
+  else
+   status
  in
   GrafiteTypes.Serializer.register#run "ncoercion" aux_l 
 ;;
 
 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