GrafiteTypes.universe = universe},
lemmas
-let add_coercion refinement_toolkit ~add_composites status uri arity baseuri =
+let add_coercion refinement_toolkit ~add_composites status uri arity
+ saturations baseuri
+=
let compounds =
- LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity baseuri in
+ LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity
+ saturations baseuri in
{status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
compounds