]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/librarySync.ml
removed some refinement_toolkit
[helm.git] / helm / software / components / library / librarySync.ml
index e621a7a0cf1311ef26319e7363714db36fce5383..8ecabbbb6aeb435b44c735d744d709f37b97007a 100644 (file)
@@ -282,7 +282,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
     (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
   else
     let new_coercions = 
-      CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri 
+      CicCoercion.close_coercion_graph src_carr tgt_carr uri 
        baseuri
     in
     let new_coercions =