let eval_coercion status ~add_composites uri =
let basedir = Helm_registry.get "matita.basedir" in
let status,compounds =
+ prerr_endline "evaluating a coercion command";
GrafiteSync.add_coercion ~basedir ~add_composites status uri in
let moo_content = coercion_moo_statement_of uri in
let status = GrafiteTypes.add_moo_content [moo_content] status in
None)
lemmas)
in
+ prerr_endline "actual coercions:";
List.iter
(fun u -> prerr_endline (UriManager.string_of_uri u))
coercions;
- 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
let add_obj uri obj status =
let basedir = Helm_registry.get "matita.basedir" in