]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/nCicCoercDeclaration.ml
added auto_cache in the dupable status after an
[helm.git] / helm / software / components / grafite_engine / nCicCoercDeclaration.ml
index 2f103cf83f944fe2255a908cf7c10779803b4da1..ea112bf4ebb16deb048be05402c2b91f2221b24d 100644 (file)
@@ -294,7 +294,10 @@ let record_ncoercion =
  let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term =
    List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l
  in
-  NCicLibrary.Serializer.register "ncoercion" aux_l
+  NCicLibrary.Serializer.register#run "ncoercion"
+   object(self : 'a NCicLibrary.register_type)
+    method run = aux_l 
+   end
 ;;
 
 let basic_eval_and_record_ncoercion infos status =