+ | 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 status = ref status in
+ !eval_from_stream_ref status stream (fun _ _ -> ());
+ !status
+ | TacticAst.Set (loc, name, value) ->
+ let value =
+ if name = "baseuri" then
+ MatitaMisc.strip_trailing_slash value
+ else
+ value
+ in
+ set_option status name value
+ | TacticAst.Drop loc -> raise Drop