From 152d8a93bbb70ca6ad6a7cd629bd508fd16c1a44 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 23 Feb 2015 19:08:08 +0100
Subject: Fixed doc of fresh (was already outdated before fixing #3233).

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

(limited to 'doc')

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}.
-- 
cgit v1.2.3


From 9582053a841c55010ddb2c4868f691151d4d949d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Feb 2015 15:32:02 +0100
Subject: Fixing bug 3099.

---
 doc/refman/Classes.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc')

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$} :
-- 
cgit v1.2.3