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

7 files changed, 50 insertions, 25 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 9bcca85895..dd6bcba85a 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 20444dc0a1..9d88fa077e 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 cac0b0f769..b5684f929a 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 3e3d422638..3a4d7f03e6 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 5cbe9c61b2..d158590479 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 7ef9078db4..d5c6dbfdb9 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 396f3464e6..2e589e4716 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
+}