diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index 1de805d0e2..4fd1fdd480 100644 --- a/src/library/tactic/tactic_state.h +++ b/src/library/tactic/tactic_state.h @@ -153,6 +153,7 @@ template tactic_state update_option_if_undef(tactic_state const & s, return set_options(s, s.get_options().update_if_undef(n, v)); } +bool is_ts_safe(tactic_state const & s); typedef interaction_monad tactic; vm_obj to_obj(tactic_state const & s);