diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-02-23 19:08:08 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-02-23 19:08:08 +0100 |
| commit | 152d8a93bbb70ca6ad6a7cd629bd508fd16c1a44 (patch) | |
| tree | ced66318b7f2ee36fce068ad73dc88641f33d2e6 /doc | |
| parent | cea92f33654bf924f5be861a946ee5084eca840b (diff) | |
Fixed doc of fresh (was already outdated before fixing #3233).
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index eea53886b..186bc9add 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -142,7 +142,7 @@ is understood as & | & {\tt idtac} \sequence{\messagetoken}{}\\ & | & {\tt fail} \zeroone{\naturalnumber} \sequence{\messagetoken}{}\\ & | & {\tt gfail} \zeroone{\naturalnumber} \sequence{\messagetoken}{}\\ -& | & {\tt fresh} ~|~ {\tt fresh} {\qstring}\\ +& | & {\tt fresh} ~|~ {\tt fresh} {\qstring}|~ {\tt fresh} {\qualid}\\ & | & {\tt context} {\ident} {\tt [} {\term} {\tt ]}\\ & | & {\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\ & | & {\tt type of} {\term}\\ @@ -906,8 +906,8 @@ The following expression returns an identifier: \end{quote} It evaluates to an identifier unbound in the goal. This fresh identifier is obtained by concatenating the value of the -\textrm{\textsl{component}}'s (each of them is, either an {\ident} which -has to refer to a name, or directly a name denoted by a +\textrm{\textsl{component}}'s (each of them is, either an {\qualid} which +has to refer to a (unqualified) name, or directly a name denoted by a {\qstring}). If the resulting name is already used, it is padded with a number so that it becomes fresh. If no component is given, the name is a fresh derivative of the name {\tt H}. |