+ let statement_of name =
+ TacticAstPp.pp_statement
+ (TacticAst.Executable (CicAst.dummy_floc,
+ (TacticAst.Command (CicAst.dummy_floc,
+ (TacticAst.Coercion (CicAst.dummy_floc,
+ (CicAst.Ident (name, None)))))))) ^ "\n"
+ in
+ let moo_content_rev =
+ [statement_of (UriManager.name_of_uri coer_uri)] @
+ (List.map
+ (fun (uri, _, _) ->
+ statement_of (UriManager.name_of_uri uri))
+ new_coercions) @ status.moo_content_rev
+ in
+ let status = {status with moo_content_rev = moo_content_rev} in