let obj = Cic.Constant (name,Some bo,ty,[],[]) in
MatitaSync.add_obj uri obj status
| TacticAst.Coercion (loc, coercion) ->
- eval_coercion status coercion
+ let status = eval_coercion status coercion in
+ let moo_content_rev =
+ (TacticAstPp.pp_cic_command
+ (TacticAst.Coercion (CicAst.dummy_floc,coercion)) ^ ".\n") ::
+ status.moo_content_rev in
+ {status with moo_content_rev = moo_content_rev}
| TacticAst.Alias (loc, spec) ->
let aliases =
match spec with