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(-)

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