let new_coercions =
CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
let status =
- List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status)
+ List.fold_left (fun s (uri,o,_) ->
+ let status = MatitaSync.add_obj uri o status in
+ {status with coercions = uri :: status.coercions})
status new_coercions in
+ let status = {status with coercions = coer_uri :: status.coercions} in
let statement_of name =
GrafiteAst.Coercion (DisambiguateTypes.dummy_floc,
(CicNotationPt.Ident (name, None)))
proof_status = No_proof;
options = default_options ();
objects = [];
+ coercions = [];
notation_ids = [];
}