Backporting from v8.2 to trunk:

- Filtering of doc compilation messages (11793,11795,11796).
- Fixing bug #1925 and cleaning around bug #1894 (11796, 11801).
- Adding some tests.



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

14 files changed, 113 insertions, 36 deletions

diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex
index 56c4f172a..79b4f7f1a 100644
--- a/doc/RecTutorial/RecTutorial.tex
+++ b/doc/RecTutorial/RecTutorial.tex
@@ -2421,7 +2421,7 @@ Fixpoint plus' (n p:nat) \{struct p\} : nat :=
 %\end{alltt}
 
 In the following definition of addition, 
-the second argument of \verb@plus''@ grows at each
+the second argument of {\tt plus{'}{'}} grows at each
 recursive call. However, as the first one always decreases, the
 definition is sound.
 \begin{alltt}
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index c27a3357e..6048a75fd 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -72,7 +72,7 @@
 %\newcommand{\spec}[1]{\{\,#1\,\}}
 
 % Building regular expressions
-\newcommand{\zeroone}[1]{{\sl [}#1{\sl ]}}
+\newcommand{\zeroone}[1]{\mbox{\sl [}#1\mbox{\sl ]}}
 %\newcommand{\zeroonemany}[1]{$\{$#1$\}$*}
 %\newcommand{\onemany}[1]{$\{$#1$\}$+}
 \newcommand{\nelist}[2]{{#1} {\tt #2} {\ldots} {\tt #2} {#1}}
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 0644cf369..a21de8f24 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -596,7 +596,7 @@ Proof-irrelevance (in {\Prop}) can be assumed without contradiction in
 form of the proof is. This is in harmony with the common purely
 logical interpretation of {\Prop}. Contrastingly, proof-irrelevance is
 inconsistent in {\Set} since there are types in {\Set}, such as the
-type of booleans, that are provably more than 2 elements.
+type of booleans, that provably have at least two distinct elements.
 
 Proof-irrelevance (in {\Prop}) is a consequence of classical logic
 (see proofs in file \vfile{\LogicClassical}{Classical} and
@@ -1863,9 +1863,9 @@ You can use for instance:
 Notation "x ^2" := (Rmult x x) (at level 20).
 \end{verbatim}
 Note that you can not use:
-\begin{texttt}
+\begin{tt}
 Notation "x $^˛$" := (Rmult x x) (at level 20).
-\end{texttt}
+\end{tt}
 because ``$^2$'' is an iso-latin character. If you really want this kind of notation you should use UTF-8.
 
 
@@ -2278,12 +2278,12 @@ and set key \texttt{gtk-key-theme} to \texttt{Emacs} in the category
 \Question{How to use those Forall and Exists pretty symbols?}\label{forallcoqide}
  Thanks to the notation features in \Coq, you just need to insert these
 lines in your {\Coq} buffer:\\
-\begin{texttt}
+\begin{tt}
 Notation "$\forall$ x : t, P" := (forall x:t, P) (at level 200, x ident).
-\end{texttt}\\
-\begin{texttt}
+\end{tt}\\
+\begin{tt}
 Notation "$\exists$ x : t, P" := (exists x:t, P) (at level 200, x ident).
-\end{texttt}
+\end{tt}
 
 Copy/Paste of these lines from this file will not work outside of \CoqIde.
 You need to load a file containing these lines or to enter the $\forall$
@@ -2531,7 +2531,7 @@ theorem proving in \Coq.
 
 %%%%%%%
 \typeout{*********************************************}
-\typeout{********* That makes \thequestion{\space} questions **********}
+\typeout{********* That makes {\thequestion} questions **********}
 \typeout{*********************************************}
 
 \end{document}
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 9bcca8589..dd6bcba85 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -2,7 +2,7 @@
 \def\eol{\setlength\parskip{0pt}\par}
 \def\indent#1{\noindent\kern#1}
 \def\cst#1{\textsf{#1}}
-\def\tele#1{\ensuremath{\overrightarrow{#1}}}
+\newcommand\tele[1]{\overrightarrow{#1}}
 
 \achapter{\protect{Type Classes}}
 \aauthor{Matthieu Sozeau}
@@ -306,7 +306,7 @@ priority as for auto hints.
   It does not include curly braces and one need not even mention
   the unique field name.
 
-\item {\tt Instance Global} One can use the \texttt{Global} modifier on
+\item {\tt Global Instance} One can use the \texttt{Global} modifier on
   instances declared in a section so that their generalization is automatically
   redeclared after the section is closed.
 
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 20444dc0a..9d88fa077 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -105,9 +105,9 @@ obligations. Once solved using the commands shown below, it binds the final
 \item {\tt Program Definition {\ident} {\binder$_1$}\ldots{\binder$_n$}
        {\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\
   This is equivalent to \\
-   {\tt Program Definition\,{\ident}\,{\tt :\,forall}\,%
-       {\binder$_1$}\ldots{\binder$_n$}{\tt ,}\,\term$_1$\,{\tt :=}}\,%
-       {\tt fun}\,{\binder$_1$}\ldots{\binder$_n$}\,{\tt =>}\,{\term$_2$}\,%
+   {\tt Program Definition\,{\ident}\,{\tt :\,forall} %
+       {\binder$_1$}\ldots{\binder$_n$}{\tt ,}\,\term$_1$\,{\tt :=}} \\
+       \qquad {\tt fun}\,{\binder$_1$}\ldots{\binder$_n$}\,{\tt =>}\,{\term$_2$}\,%
        {\tt .}
 \end{Variants}
 
diff --git a/doc/refman/RefMan-decl.tex b/doc/refman/RefMan-decl.tex
index cac0b0f76..b5684f929 100644
--- a/doc/refman/RefMan-decl.tex
+++ b/doc/refman/RefMan-decl.tex
@@ -804,6 +804,6 @@ is executed to prove the statement. The default is a solver for
 \section{More details and Formal Semantics}
 
 I suggest the users looking for more information have a look at the
-paper \cite{corbinea08types}. They will find in that paper a formal
+paper \cite{corbineau08types}. They will find in that paper a formal
 semantics of the proof state transition induces by mathematical
 commands.
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 3e3d42263..3a4d7f03e 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -880,7 +880,7 @@ These are synonyms of the {\tt Definition} forms.
 \end{Variants}
 
 \begin{ErrMsgs}
-\item \errindex{Error: The term ``{\term}'' has type "{\type}" while it is expected to have type ``{\type}''}
+\item \errindex{Error: The term ``{\term}'' has type ``{\type}'' while it is expected to have type ``{\type}''}
 \end{ErrMsgs}
 
 \SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 5cbe9c61b..d15859047 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -820,10 +820,10 @@ subdirectories:
  {\bf Reals}    & Axiomatization of real numbers (classical, basic functions, 
                   integer part, fractional part, limit, derivative, Cauchy 
                   series, power series and results,...)\\
- {\bf Relations} & Relations (definitions and basic results). \\
- {\bf Sorting}  & Sorted list (basic definitions and heapsort correctness). \\
+ {\bf Relations} & Relations (definitions and basic results) \\
+ {\bf Sorting}  & Sorted list (basic definitions and heapsort correctness) \\
  {\bf Strings}  & 8-bits characters and strings\\
- {\bf Wellfounded} & Well-founded relations (basic results). \\
+ {\bf Wellfounded} & Well-founded relations (basic results) \\
 
 \end{tabular}
 \medskip
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 7ef9078db..d5c6dbfdb 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -276,7 +276,7 @@ $v_1$. Sequence is left-associative.
 \subsubsection[General sequence]{General sequence\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}}
 %\tacindex{; [ | ]}
 %\index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}}
-\index{Tacticals!; [ | ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
+\index{Tacticals!; [ \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
 
 We can generalize the previous sequence operator as
 \begin{quote}
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 396f3464e..2e589e471 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -183,13 +183,10 @@ s},
 
 @InProceedings{ChiPotSimp03,
   author      = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson},
-  address     = {Berg en Dal, The Netherlands},
   title       = {Mathematical Quotients and Quotient Types in Coq},
-  booktitle   = {TYPES'02},
-  publisher   = SV,
-  series      = LNCS,
-  volume      = {2646},
-  year        = {2003}
+  booktitle   = {TYPES},
+  crossref    = {DBLP:conf/types/2002},
+  year        = {2002}
 }
 
 @TechReport{CoC89,
@@ -296,6 +293,19 @@ s},
   crossref    = {Nijmegen93}
 }
 
+@inproceedings{Corbineau08types,
+  author      = {P. Corbineau},
+  title       = {A Declarative Language for the Coq Proof Assistant},
+  editor      = {M. Miculan and I. Scagnetto and F. Honsell},
+  booktitle   = {TYPES '07, Cividale del Friuli, Revised Selected Papers},
+  publisher   = {Springer},
+  series      = LNCS,
+  volume      = {4941},
+  year        = {2007},
+  pages       = {69-84},
+  ee          = {http://dx.doi.org/10.1007/978-3-540-68103-8_5},
+}
+
 @PhDThesis{Cor97,
   author      = {C. Cornes},
   month       = nov,
@@ -317,7 +327,7 @@ s},
   author      = {Delahaye, D.},
   title       = {Information Retrieval in a Coq Proof Library using
                  Type Isomorphisms},
-  booktitle   = {Proceedings of TYPES'99, L\"okeberg},
+  booktitle   = {Proceedings of TYPES '99, L\"okeberg},
   publisher   = SV,
   series      = lncs,
   year        = {1999},
@@ -763,8 +773,9 @@ of the {ML} language},
 @InProceedings{Let02,
   author      = {P. Letouzey},
   title       = {A New Extraction for Coq},
-  booktitle   = {Proceedings of the TYPES'2002 workshop},
+  booktitle   = {TYPES},
   year        = 2002,
+  crossref    = {DBLP:conf/types/2002},
   url         = {draft at \url{http://www.pps.jussieu.fr/~letouzey/download/extraction2002.ps.gz}}
 }
 
@@ -823,14 +834,28 @@ Intersection Types and Subtyping},
 @InProceedings{MiWer02,
   author      = {A. Miquel and B. Werner},
   title       = {The Not So Simple Proof-Irrelevant Model of CC},
-  booktitle   = {Types for Proofs and Programs (TYPES'02)},
+  booktitle   = {TYPES},
+  year        = {2002},
+  pages       = {240-258},
+  ee          = {http://link.springer.de/link/service/series/0558/bibs/2646/26460240.htm},
+  crossref    = {DBLP:conf/types/2002},
+  bibsource   = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/types/2002,
+  editor      = {H. Geuvers and F. Wiedijk},
+  title       = {Types for Proofs and Programs, Second International Workshop,
+                 TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002,
+                 Selected Papers},
+  booktitle   = {TYPES},
   publisher   = SV,
-  series      = {LNCS},
-  number      = 2646,
-  year        = 2003
+  series      = LNCS,
+  volume      = {2646},
+  year        = {2003},
+  isbn        = {3-540-14031-X},
+  bibsource   = {DBLP, http://dblp.uni-trier.de}
 }
 
-
 @InProceedings{Moh89a,
   author      = {C. Paulin-Mohring},
   address     = {Austin},
@@ -1236,4 +1261,4 @@ Languages},
     journal = "Communication of the ACM",
     pages = "102--114",
     year = "1992",
-}
\ No newline at end of file
+}
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 84e4e4fa0..64bf252f2 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -308,6 +308,7 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
     theories/Classes/Morphisms_Relations.v
     theories/Classes/Equivalence.v
     theories/Classes/EquivDec.v
+    theories/Classes/Functions.v
     theories/Classes/SetoidTactics.v
     theories/Classes/SetoidClass.v
     theories/Classes/SetoidDec.v
diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files
index 9516a19ff..39cedbec4 100755
--- a/doc/stdlib/make-library-files
+++ b/doc/stdlib/make-library-files
@@ -10,7 +10,7 @@
 # En supposant que make fait son boulot, ca fait un tri topologique du
 # graphe des dépendances
 
-LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes"
+LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes Numbers"
 
 rm -f library.files.ls.tmp
 (cd $COQSRC/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp
diff --git a/doc/tools/latex_filter b/doc/tools/latex_filter
new file mode 100644
index 000000000..4b6e1a869
--- /dev/null
+++ b/doc/tools/latex_filter
@@ -0,0 +1,43 @@
+#!/bin/sh
+
+# First argument is the number of lines to treat
+# Second argument is optional and, if it is "no", overfull are not displayed
+
+i=$1
+nooverfull=$2
+error=0
+verbose=0
+chapter=""
+file=""
+while : ; do 
+  read -r line; 
+  case $line in
+    "! "*)
+      echo $line $file;
+      error=1
+      verbose=1
+      ;;
+    "LaTeX Font Info"*|"LaTeX Info"*|"Underfull "*)
+      verbose=0
+      ;;
+    "Overfull "*)
+      verbose=0
+      if [ "$nooverfull" != "no" ]; then echo $line $file; fi
+      ;;
+    "LaTeX "*)
+      verbose=0
+      echo $line $chapter
+      ;;
+    "["*|"Chapter "*)
+      verbose=0
+      ;;
+    "(./"*)
+      file="(file `echo $line | cut -b 4- | cut -d' ' -f 1`)"
+      verbose=0
+      ;;
+    *)
+      if [ $verbose == 1 ]; then echo $line; fi
+  esac;
+  if [ "$i" == "0" ]; then break; else i=`expr $i - 1`; fi; 
+done
+exit $error
diff --git a/doc/tools/show_latex_messages b/doc/tools/show_latex_messages
new file mode 100644
index 000000000..87b463806
--- /dev/null
+++ b/doc/tools/show_latex_messages
@@ -0,0 +1,8 @@
+#!/bin/sh
+
+if [ "$1" == "-no-overfull" ]; then
+  ../tools/latex_filter `wc -l < $2` no < $2
+else
+  ../tools/latex_filter `wc -l < $1` yes < $1
+fi
+