]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/grafite_engine/nCicCoercDeclaration.ml
WARNING: partial commit (does not compile)
[helm.git] / matita / components / grafite_engine / nCicCoercDeclaration.ml
index 3cf07626531c37902cff53640451885386211997..8ba2f92f88d5c1b2d60fe70771fbc2a80d010650 100644 (file)
@@ -291,10 +291,7 @@ 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#run "ncoercion"
-   object(self : 'a NCicLibrary.register_type)
-    method run = aux_l 
-   end
+  GrafiteTypes.Serializer.register#run "ncoercion" aux_l 
 ;;
 
 let basic_eval_and_record_ncoercion infos status =