\DOC FAIL_TAC

\TYPE {FAIL_TAC : string -> tactic}

\SYNOPSIS
Tactic that always fails, with the supplied string.

\KEYWORDS
tactic.

\DESCRIBE
Whatever goal it is applied to, {FAIL_TAC "s"} always fails with {Failure "s"}.

\FAILURE
The application of {FAIL_TAC} to a string never fails; the resulting
tactic always fails.

\EXAMPLE
The following example uses the fact that if a tactic {t1} solves
a goal, then the tactic {t1 THEN t2} never results in the application
of {t2} to anything, because {t1} produces no subgoals. In attempting
to solve the following goal:
{
  # g `if x then T else T`;;
}
\noindent the tactic
{
  # e(REWRITE_TAC[] THEN FAIL_TAC "Simple rewriting failed to solve goal");;
  Exception: Failure "Simple rewriting failed to solve goal".
}
\noindent fails with the message provided, whereas the following quietly solves
the goal:
{
  # e(REWRITE_TAC[COND_ID] THEN FAIL_TAC "Using that failed to solve goal");;
  val it : goalstack = No subgoals
}

\SEEALSO
ALL_TAC, NO_TAC.

\ENDDOC