Fix examples in Program documentation and add comindexes for the various

commands. Update documentation of implicit arguments with the new syntax
and an explanation for the way it works in inductive type definitions.


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

3 files changed, 38 insertions, 16 deletions

diff --git a/Makefile.doc b/Makefile.doc
index fedde37483..3705c047a2 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -86,7 +86,7 @@ doc/refman/Reference-Manual.dvi: $(DOCCOMMON) $(REFMANFILES)
 	$(LATEX) Reference-Manual;\
 	$(LATEX) Reference-Manual)
 
-doc/refman/Reference-Manual.pdf: doc/refman/Reference-Manual.tex
+doc/refman/Reference-Manual.pdf: $(REFMANFILES) doc/refman/Reference-Manual.tex
 	(cd doc/refman; $(PDFLATEX) Reference-Manual.tex)
 
 ### Reference Manual (browsable format)
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 6e3cb4c4b2..e06e3e70e1 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -133,6 +133,7 @@ The structural fixpoint operator behaves just like the one of Coq
 It works with mutually recursive definitions too.
 
 \begin{coq_example}
+Require Import Program.
 Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
   match n with
   | S (S p) => S (div2 p)
@@ -150,11 +151,12 @@ You can use a well-founded order or a measure as termination orders using the sy
 \begin{coq_eval}
 Reset Initial.
 Require Import Arith.
+Require Import Program.
 \end{coq_eval}
 \begin{coq_example}
 Definition id (n : nat) := n.
-
-Program Fixpoint div2 (n : nat) {measure id n} : { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
+Program Fixpoint div2 (n : nat) {measure id n} :
+  { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
   match n with
   | S (S p) => S (div2 p)
   | _ => O
@@ -206,23 +208,27 @@ obligations (e.g. when defining mutually recursive blocks). The optional
 tactic is replaced by the default one if not specified.
 
 \begin{itemize}
-\item {\tt Obligations Tactic := \tacexpr} Sets the default obligation
+\item {\tt Obligations Tactic := \tacexpr}\comindex{Obligations Tactic}
+  Sets the default obligation
   solving tactic applied to all obligations automatically, whether to
   solve them or when starting to prove one, e.g. using {\tt Next}.
-\item {\tt Obligations [of \ident]} Displays all remaining
+\item {\tt Obligations [of \ident]}\comindex{Obligations} Displays all remaining
   obligations.
-\item {\tt Next Obligation [of \ident]} Start the proof of the next
-  unsolved obligation.
-\item {\tt Obligation num [of \ident]} Start the proof of
+\item {\tt Obligation num [of \ident]}\comindex{Obligation} Start the proof of
   obligation {\tt num}.
-\item {\tt Solve Obligations [of \ident] [using \tacexpr]} Tries to solve
+\item {\tt Next Obligation [of \ident]}\comindex{Next Obligation} Start the proof of the next
+  unsolved obligation.
+\item {\tt Solve Obligations [of \ident] [using
+    \tacexpr]}\comindex{Solve Obligations}
+  Tries to solve
   each obligation of \ident using the given tactic or the default one.
 \item {\tt Solve All Obligations [using \tacexpr]} Tries to solve
   each obligation of every program using the given tactic or the default
   one (useful for mutually recursive definitions).
-\item {\tt Admit Obligations [of \ident]} Admits all
-  obligations (does not work with structurally recursive programs).
-\item {\tt Preterm [of \ident]} Shows the term that will be fed to
+\item {\tt Admit Obligations [of \ident]}\comindex{Admit Obligations} 
+  Admits all obligations (does not work with structurally recursive programs).
+\item {\tt Preterm [of \ident]}\comindex{Preterm} 
+  Shows the term that will be fed to
   the kernel once the obligations are solved. Useful for debugging.
 \end{itemize}
 
@@ -231,7 +237,6 @@ obligations called {\tt program\_simpl}. Importing
 {\tt Coq.Program.Program} also adds some useful notations, as documented in the file itself.
 
 \section{Frequently Asked Questions
-  \comindex{Program FAQ}
   \label{ProgramFAQ}}
 
 \begin{itemize}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 5dc06f33cc..de6b93b424 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1133,23 +1133,40 @@ a-priori and a-posteriori.
 
 In the first setting, one wants to explicitely give the implicit
 arguments of a constant as part of its definition. To do this, one has
-to surround the bindings of implicit arguments by backquotes:
+to surround the bindings of implicit arguments by curly braces:
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
-Definition id `A : Type` (x : A) : A := x.
+Definition id {A : Type} (x : A) : A := x.
 \end{coq_example}
 
 This automatically declares the argument {\tt A} of {\tt id} as a
 maximally inserted implicit argument. One can then do as-if the argument
 was absent in every situation but still be able to specify it if needed:
 \begin{coq_example}
-Definition compose `A B C` (g : B -> C) (f : A -> B) := 
+Definition compose {A B C} (g : B -> C) (f : A -> B) := 
   fun x => g (f x).
 Goal forall A, compose id id = id (A:=A).
 \end{coq_example}
 
+The syntax is supported in all top-level definitions: {\tt Definition},
+{\tt Fixpoint}, {\tt Lemma} and so on. For (co-)inductive datatype
+declarations, the semantics are the following: an inductive parameter
+declared as an implicit argument need not be repeated in the inductive
+definition but will become implicit for the constructors of the
+inductive only, not the inductive type itself. For example:
+
+\begin{coq_example}
+Inductive list {A : Type} : Type :=
+| nil : list
+| cons : A -> list -> list.
+Print list.
+\end{coq_example}
+
+One can always specify the parameter if it is not uniform using the
+usual implicit arguments disambiguation syntax.
+
 \subsubsection{The Implicit Arguments Vernacular Command}
 
 To set implicit arguments for a constant a-posteriori, one can use the