let eval_command status cmd =
match cmd with
+ | TacticAst.Default (loc, what, uris) as cmd ->
+ LibraryObjects.set_default what uris;
+ {status with moo_content_rev =
+ (TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
| TacticAst.Include (loc, path) ->
let path = MatitaMisc.obj_file_of_script path in
let stream = Stream.of_channel (open_in path) in
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
status, tacticals
let disambiguate_command status = function
- | TacticAst.Include (loc,path) as cmd -> status,cmd
+ | TacticAst.Default _
+ | TacticAst.Alias _
+ | TacticAst.Include _ as cmd -> status,cmd
| TacticAst.Coercion (loc, term) ->
let status, term = disambiguate_term status term in
status, TacticAst.Coercion (loc,term)
| (TacticAst.Set _ | TacticAst.Qed _ | TacticAst.Drop _ ) as cmd ->
status, cmd
- | TacticAst.Alias _ as x -> status, x
| TacticAst.Obj (loc,obj) ->
let status,obj = disambiguate_obj status obj in
status, TacticAst.Obj (loc,obj)