- let status = GrafiteTypes.add_moo_content moo_content status in
- let basedir = Helm_registry.get "matita.basedir" in
- List.fold_left
- (fun (status,lemmas) uri ->
- let status,new_lemmas =
- GrafiteSync.add_coercion ~basedir ~add_composites:true status uri
- in
- status,new_lemmas@lemmas
- ) (status,[]) coercions
+ let status = GrafiteTypes.add_moo_content moo_content status in
+ {status with
+ GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions},
+ lemmas