- let compounds =
- LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity
- saturations 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 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