From 480b645dcebc8b8a91615526e1d2717699a5a7c7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 24 May 2017 17:25:08 +0200
Subject: Documenting the existence of first and solve as Ltac definitions.

---
 doc/refman/RefMan-ltac.tex | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 0346c4a555..bb679ecba7 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}}}
 
-- 
cgit v1.2.3