-let add_coercion refinement_toolkit ~add_composites status uri arity baseuri =
- let compounds =
- LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity baseuri in
- {status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
- compounds
-
-module OrderedUri =
-struct
- type t = UriManager.uri * string
- let compare (u1, _) (u2, _) = UriManager.compare u1 u2
-end
-
-module UriSet = Set.Make (OrderedUri)
+let add_coercion ~pack_coercion_obj ~add_composites status uri arity
+ saturations baseuri
+=
+ let lemmas =
+ LibrarySync.add_coercion ~add_composites ~pack_coercion_obj
+ uri arity saturations baseuri in
+ { status with GrafiteTypes.coercions = CoercDb.dump () ;
+ objects = lemmas @ status.GrafiteTypes.objects
+ },
+ lemmas