diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 0346c4a55..bb679ecba 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -522,6 +522,19 @@ to have \emph{at least} one success. \ErrMsg \errindex{No applicable tactic} +\variant {\tt first {\tacexpr}} + +This is an Ltac alias that gives a primitive access to the {\tt first} tactical +as a Ltac definition without going through a parsing rule. It expects to be +given a list of tactics through a {\tt Tactic Notation}, allowing to write +notations of the following form. + +\Example + +\begin{quote} +{\tt Tactic Notation "{foo}" tactic\_list(tacs) := first tacs.} +\end{quote} + \subsubsection[Left-biased branching]{Left-biased branching\tacindex{$\mid\mid$} \index{Tacticals!orelse@{\tt $\mid\mid$}}} @@ -600,6 +613,11 @@ $v_2$ and so on. It fails if there is no solving tactic. \ErrMsg \errindex{Cannot solve the goal} +\variant {\tt solve {\tacexpr}} + +This is an Ltac alias that gives a primitive access to the {\tt solve} tactical. +See the {\tt first} tactical for more information. + \subsubsection[Identity]{Identity\label{ltac:idtac}\tacindex{idtac} \index{Tacticals!idtac@{\tt idtac}}} |