diff options
| author | Pierre-Marie Pédrot | 2017-07-04 14:38:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-04 14:52:37 +0200 |
| commit | 8155ba54ae39dd71c6b8ddff2b2b7353dde9aff8 (patch) | |
| tree | 94b2b61cd034873c537b7991cdbe6312fdad2fb3 /doc/refman/RefMan-ltac.tex | |
| parent | 3e0334dd48b5d0b03046d0aff1a82867dc98d656 (diff) | |
| parent | e0ad7ac11b97f089fa862d2e34409e0a1d77d3a1 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'doc/refman/RefMan-ltac.tex')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index bb679ecba7..f3bc2dd05e 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -392,7 +392,7 @@ all selected goals. \item{} [{\ident}] {\tt :} {\tacexpr} In this variant, {\tacexpr} is applied locally to a goal - previously named by the user. + previously named by the user (see~\ref{ExistentialVariables}). \item {\num} {\tt :} {\tacexpr} @@ -891,7 +891,7 @@ behavior can be retrieved with the {\tt Tactic Compat Context} flag. \end{Variants} -\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}} +\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}\label{ltac-match-goal} \index{Ltac!match reverse goal@\texttt{match reverse goal}} \index{match goal@\texttt{match goal}!in Ltac} \index{match reverse goal@\texttt{match reverse goal}!in Ltac}} |