Documentation of Arguments + implicits

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

1 files changed, 67 insertions, 30 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 3429bafabf..47a2e462dd 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1141,7 +1141,7 @@ possible, the correct argument will be automatically generated.
 \end{ErrMsgs}
 
 \subsection{Declaration of implicit arguments for a constant
-\comindex{Implicit Arguments}}
+\comindex{Arguments}}
 \label{ImplicitArguments}
 
 In case one wants that some arguments of a given object (constant,
@@ -1188,44 +1188,44 @@ Print list.
 One can always specify the parameter if it is not uniform using the
 usual implicit arguments disambiguation syntax.
 
-\subsubsection{The Implicit Arguments Vernacular Command}
+\subsubsection{Declaring Implicit Arguments}
 
 To set implicit arguments for a constant a-posteriori, one can use the
 command:
 \begin{quote}
-\tt Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ]
+\tt Arguments {\qualid} \nelist{\possiblybracketedident}{}
 \end{quote}
-where the list of {\possiblybracketedident} is the list of parameters
-to be declared implicit, each of the identifier of the list being
-optionally surrounded by square brackets, then meaning that this
-parameter has to be maximally inserted.
+where the list of {\possiblybracketedident} is the list of all arguments of
+{\qualid} where the ones to be declared implicit are surrounded by
+square brackets and the ones to be declared as maximally inserted implicits
+are surrounded by curly braces.
 
 After the above declaration is issued, implicit arguments can just (and
 have to) be skipped in any expression involving an application of
 {\qualid}.
 
 \begin{Variants}
-\item {\tt Global Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ]
-\comindex{Global Implicit Arguments}}
+\item {\tt Global Arguments {\qualid} \nelist{\possiblybracketedident}{}
+\comindex{Global Arguments}}
 
 Tells to recompute the implicit arguments of {\qualid} after ending of
 the current section if any, enforcing the implicit arguments known
 from inside the section to be the ones declared by the command.
 
-\item {\tt Local Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ]
-\comindex{Local Implicit Arguments}}
+\item {\tt Local Arguments {\qualid} \nelist{\possiblybracketedident}{}
+\comindex{Local Arguments}}
 
 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}{} ]}{}}
+\item {\tt \zeroone{Global {\sl |} Local} 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
+instance constants whose type is polymorphic), multiple 
+implicit arguments decflarations can be given. 
+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.
 
@@ -1245,17 +1245,17 @@ Inductive list (A:Type) : Type :=
 \end{coq_example*}
 \begin{coq_example}
 Check (cons nat 3 (nil nat)).
-Implicit Arguments cons [A].
-Implicit Arguments nil [A].
+Arguments cons [A] _ _.
+Arguments nil [A].
 Check (cons 3 nil).
 Fixpoint map (A B:Type) (f:A->B) (l:list A) : list B :=
   match l with nil => nil | cons a t => cons (f a) (map A B f t) end.
 Fixpoint length (A:Type) (l:list A) : nat :=
   match l with nil => 0 | cons _ m => S (length A m) end.
-Implicit Arguments map [A B].
-Implicit Arguments length [[A]]. (* A has to be maximally inserted *)
+Arguments map [A B] f l.
+Arguments length {A} l. (* A has to be maximally inserted *)
 Check (fun l:list (list nat) => map length l).
-Implicit Arguments map [A B] [A] [].
+Arguments map [A B] f l, [A] B f l, A B f l.
 Check (fun l => map length l = map (list nat) nat length l).
 \end{coq_example}
 
@@ -1270,8 +1270,8 @@ implicit arguments of {\qualid}.
 {\Coq} can also automatically detect what are the implicit arguments
 of a defined object. The command is just
 \begin{quote}
-{\tt Implicit Arguments {\qualid}
-\comindex{Implicit Arguments}}
+{\tt Arguments {\qualid} : default implicits
+\comindex{Arguments}}
 \end{quote}
 The auto-detection is governed by options telling if strict,
 contextual, or reversible-pattern implicit arguments must be
@@ -1280,14 +1280,14 @@ Sections~\ref{SetStrictImplicit},~\ref{SetContextualImplicit},~\ref{SetReversibl
 and also~\ref{SetMaximalImplicitInsertion}).
 
 \begin{Variants}
-\item {\tt Global Implicit Arguments {\qualid}
-\comindex{Global Implicit Arguments}}
+\item {\tt Global Arguments {\qualid} : default implicits
+\comindex{Global Arguments}}
 
 Tells to recompute the implicit arguments of {\qualid} after ending of
 the current section if any.
 
-\item {\tt Local Implicit Arguments {\qualid}
-\comindex{Local Implicit Arguments}}
+\item {\tt Local Arguments {\qualid} : default implicits
+\comindex{Local Arguments}}
 
 When in a module, tells not to activate the implicit arguments of
 {\qualid} computed by this declaration to contexts that requires the
@@ -1305,12 +1305,12 @@ Inductive list (A:Set) : Set :=
   | cons : A -> list A -> list A.
 \end{coq_example*}
 \begin{coq_example}
-Implicit Arguments cons.
+Arguments cons : default implicits.
 Print Implicit cons.
-Implicit Arguments nil.
+Arguments nil : default implicits.
 Print Implicit nil.
 Set Contextual Implicit.
-Implicit Arguments nil.
+Arguments nil : default implicits.
 Print Implicit nil.
 \end{coq_example}
 
@@ -1326,7 +1326,7 @@ Definition Relation := X -> X -> Prop.
 Definition Transitivity (R:Relation) :=
   forall x y:X, R x y -> forall z:X, R y z -> R x z.
 Variables (R : Relation) (p : Transitivity R).
-Implicit Arguments p.
+Arguments p : default implicits.
 \end{coq_example*}
 \begin{coq_example}
 Print p.
@@ -1339,6 +1339,21 @@ Variables (a b c : X) (r1 : R a b) (r2 : R b c).
 Check (p r1 r2).
 \end{coq_example}
 
+Implicit arguments can be cleared with the following syntax:
+
+\begin{quote}
+{\tt Arguments {\qualid} : clear implicits
+\comindex{Arguments}}
+\end{quote}
+
+In the following example implict arguments declarations for the {\tt nil}
+constant are cleared:
+\begin{coq_example}
+Arguments cons : clear implicits.
+Print Implicit cons.
+\end{coq_example}
+
+
 \subsection{Mode for automatic declaration of implicit arguments
 \label{Auto-implicit}
 \comindex{Set Implicit Arguments}
@@ -1464,6 +1479,28 @@ Check (p r1 (z:=c)).
 Check (p (x:=a) (y:=b) r1 (z:=c) r2).
 \end{coq_example}
 
+\subsection{Renaming implicit arguments
+\comindex{Arguments}
+}
+
+Implicit arguments names can be redefined using the following syntax:
+\begin{quote}
+{\tt Arguments {\qualid} \nelist{\name}{}  : rename}
+\end{quote}
+
+Without the {\tt rename} flag, {\tt Arguments} can be used to assert
+that a given constant has the expected number of arguments and that
+these arguments are named as expected.
+
+\noindent {\bf Example (continued): }
+\begin{coq_example}
+Arguments p [s t] _ [u] _: rename.
+Check (p r1 (u:=c)).
+Check (p (s:=a) (t:=b) r1 (u:=c) r2).
+Fail Arguments p [s t] _ [w] _.
+\end{coq_example}
+
+
 \subsection{Displaying what the implicit arguments are
 \comindex{Print Implicit}
 \label{PrintImplicit}}