Added multiple implicit arguments rules per name.

Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]".

This should a priori be used with care (it might be a bit disturbing
seeing the same constant used with apparently incompatible signatures).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 0 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 13aef43c76..206607911b 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1205,6 +1205,19 @@ When in a module, tells not to activate the implicit arguments of
 {\qualid} declared by this commands to contexts that requires the
 module.
 
+\item {\tt \zeroone{Global {\sl |} Local} Implicit Arguments {\qualid} \sequence{[ \nelist{\possiblybracketedident}{} ]}{}}
+
+For names of constants, inductive types, constructors, lemmas which
+can only be applied to a fixed number of arguments (this excludes for
+instance constants whose type is polymorphic), multiple lists
+of implicit arguments can be given. These lists must be of different
+length, and, depending on the number of arguments {\qualid} is applied
+to in practice, the longest applicable list of implicit arguments is
+used to select which implicit arguments are inserted.
+
+For printing, the omitted arguments are the ones of the longest list
+of implicit arguments of the sequence.
+
 \end{Variants}
 
 \Example
@@ -1228,6 +1241,8 @@ Fixpoint length (A:Type) (l:list A) : nat :=
 Implicit Arguments map [A B].
 Implicit Arguments length [[A]]. (* A has to be maximally inserted *)
 Check (fun l:list (list nat) => map length l).
+Implicit Arguments map [A B] [A] [].
+Check (fun l => map length l = map (list nat) nat length l).
 \end{coq_example}
 
 \Rem To know which are the implicit arguments of an object, use the command