diff options
| author | Pierre-Marie Pédrot | 2015-02-26 17:23:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-26 17:23:58 +0100 |
| commit | 93db616a6cbebf37f2f4f983963a87a4f66972e7 (patch) | |
| tree | 94577e8d2128fd35c449acb017a637e81a701ed5 /doc | |
| parent | 31c8c317affc8fb0ae818336c70ba210208249cc (diff) | |
| parent | bc7d29e4c0f53d5c8e654157c4137c7e82910a7a (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/Classes.tex | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 6 |
2 files changed, 5 insertions, 4 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 96b486cdfa..069b991274 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -326,7 +326,8 @@ An arbitrary context of the form {\tt \binder$_1$ \ldots \binder$_n$} can be put after the name of the instance and before the colon to declare a parameterized instance. An optional \textit{priority} can be declared, 0 being the highest -priority as for auto hints. +priority as for auto hints. If the priority is not specified, it defaults to +$n$, the number of binders of the instance. \begin{Variants} \item {\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} : diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index eea53886b8..186bc9add3 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}. |