(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* add_rty; edit_at : edit_at_sty -> edit_at_rty; query : query_sty -> query_rty; goals : goals_sty -> goals_rty; evars : evars_sty -> evars_rty; hints : hints_sty -> hints_rty; status : status_sty -> status_rty; search : search_sty -> search_rty; get_options : get_options_sty -> get_options_rty; set_options : set_options_sty -> set_options_rty; mkcases : mkcases_sty -> mkcases_rty; about : about_sty -> about_rty; stop_worker : stop_worker_sty -> stop_worker_rty; print_ast : print_ast_sty -> print_ast_rty; annotate : annotate_sty -> annotate_rty; handle_exn : handle_exn_sty -> handle_exn_rty; init : init_sty -> init_rty; quit : quit_sty -> quit_rty; (* for internal use (fake_id) only, do not use *) wait : wait_sty -> wait_rty; (* Retrocompatibility stuff *) interp : interp_sty -> interp_rty; }