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

33 files changed, 328 insertions, 134 deletions

diff --git a/Makefile.common b/Makefile.common
index d9d9f2ea0..efc3bb7ef 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -80,7 +80,7 @@ HEVEA:=hevea
 HEVEAOPTS:=-fix -exec xxdate.exe
 HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea
 export TEXINPUTS:=$(COQSRC)/doc:$(HEVEALIB):
-COQTEXOPTS:=-n 72 -image "$(COQSRC)/$(COQTOPEXE) -boot" -v -sl -small
+COQTEXOPTS:=-n 72 -image "$(COQSRC)/$(COQTOPEXE) -boot" -sl -small
 
 DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex 
 
diff --git a/Makefile.doc b/Makefile.doc
index 1fbfde19b..5afd12393 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -45,16 +45,28 @@ rectutorial: doc/RecTutorial/RecTutorial.v.html \
 ### Implicit rules
 ######################################################################
 
+ifeq ($(QUICK),1)
+%.v.tex: %.tex
+	(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
+else
 %.v.tex: %.tex | $(COQTEX) $(COQTOPEXE) $(CONTRIBVO) $(CONTRIBCMO) $(THEORIESVO) 
 	(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
+endif
 
 %.ps: %.dvi
-	(cd `dirname $<`; dvips -o `basename $@` `basename $<`)
+	(cd `dirname $<`; dvips -q -o `basename $@` `basename $<`)
 
 %.eps: %.png
 	pngtopnm $< | pnmtops -equalpixels -noturn -rle > $@
 
 ######################################################################
+# Macros for filtering outputs
+######################################################################
+
+HIDEBIBTEXINFO=| grep -v "^A level-1 auxiliary file"
+SHOWMAKEINDEXERROR=egrep "^!! Input index error|^** Input style error|^   --"
+
+######################################################################
 # Common
 ######################################################################
 
@@ -73,19 +85,26 @@ doc/common/version.tex: config/Makefile
 # The second LATEX compilation is necessary otherwise the pages of the index
 # are not correct (don't know why...) - BB
 doc/refman/Reference-Manual.dvi: $(DOCCOMMON) $(REFMANFILES) doc/refman/Reference-Manual.tex
-	(cd doc/refman;\
-	$(LATEX) Reference-Manual;\
-	$(BIBTEX) Reference-Manual;\
-	$(LATEX) Reference-Manual;\
-	$(MAKEINDEX) Reference-Manual;\
-	$(MAKEINDEX) Reference-Manual.tacidx -o Reference-Manual.tacind;\
-	$(MAKEINDEX) Reference-Manual.comidx -o Reference-Manual.comind;\
-	$(MAKEINDEX) Reference-Manual.erridx -o Reference-Manual.errind;\
-	$(LATEX) Reference-Manual;\
-	$(LATEX) Reference-Manual)
+	@(cd doc/refman;\
+	$(LATEX) -interaction=batchmode Reference-Manual;\
+	$(BIBTEX) -terse Reference-Manual $(HIDEBIBTEXINFO);\
+	$(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\
+	$(MAKEINDEX) -q Reference-Manual;\
+	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
+	$(MAKEINDEX) -q Reference-Manual.tacidx -o Reference-Manual.tacind;\
+	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
+	$(MAKEINDEX) -q Reference-Manual.comidx -o Reference-Manual.comind;\
+	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
+	$(MAKEINDEX) -q Reference-Manual.erridx -o Reference-Manual.errind;\
+	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
+	$(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\
+	$(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\
+ 	../tools/show_latex_messages -no-overfull Reference-Manual.log)
 
 doc/refman/Reference-Manual.pdf: $(REFMANFILES) doc/refman/Reference-Manual.tex
-	(cd doc/refman; $(PDFLATEX) Reference-Manual.tex)
+	(cd doc/refman;\
+	$(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\
+	../tools/show_latex_messages -no-overfull Reference-Manual.log)
 
 ### Reference Manual (browsable format)
 
@@ -102,20 +121,24 @@ doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
 	$(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html
 
 refman-quick:
-	(cd doc/refman; \
-	 $(PDFLATEX) Reference-Manual.tex; \
-	 $(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex)
-
+	(cd doc/refman;\
+	$(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\
+	../tools/show_latex_messages -no-overfull Reference-Manual.log && \
+	$(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex)
 
 ######################################################################
 # Tutorial
 ######################################################################
 
 doc/tutorial/Tutorial.v.dvi: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex
-	(cd doc/tutorial; $(LATEX) Tutorial.v)
+	(cd doc/tutorial;\
+	$(LATEX) -interaction=batchmode Tutorial.v;\
+	../tools/show_latex_messages Tutorial.v.log)
 
 doc/tutorial/Tutorial.v.pdf: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex
-	(cd doc/tutorial; $(PDFLATEX) Tutorial.v.tex)
+	(cd doc/tutorial;\
+	$(PDFLATEX) -interaction=batchmode Tutorial.v.tex;\
+	../tools/show_latex_messages Tutorial.v.log)
 
 doc/tutorial/Tutorial.v.html: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex
 	(cd doc/tutorial; $(HEVEA) $(HEVEAOPTS) Tutorial.v)
@@ -127,13 +150,16 @@ doc/tutorial/Tutorial.v.html: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex
 
 doc/faq/FAQ.v.dvi: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.tex
 	(cd doc/faq;\
-	$(LATEX) FAQ.v;\
-	$(BIBTEX) FAQ.v;\
-	$(LATEX) FAQ.v;\
-	$(LATEX) FAQ.v)
+	$(LATEX) -interaction=batchmode FAQ.v;\
+	$(BIBTEX) -terse FAQ.v;\
+	$(LATEX) -interaction=batchmode FAQ.v > /dev/null;\
+	$(LATEX) -interaction=batchmode FAQ.v > /dev/null;\
+	../tools/show_latex_messages FAQ.v.log)
 
 doc/faq/FAQ.v.pdf: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.dvi doc/faq/axioms.png
-	(cd doc/faq; $(PDFLATEX) FAQ.v.tex)
+	(cd doc/faq;\
+        $(PDFLATEX) -interaction=batchmode FAQ.v.tex;\
+	../tools/show_latex_messages FAQ.v.log)
 
 doc/faq/FAQ.v.html: doc/faq/FAQ.v.dvi # to ensure FAQ.v.bbl
 	(cd doc/faq; $(HEVEA) $(HEVEAOPTS) FAQ.v.tex)
@@ -150,14 +176,23 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html
 
 ### Standard library (browsable html format)
 
+ifeq ($(QUICK),1)
+doc/stdlib/index-body.html:
+	- rm -rf doc/stdlib/html
+	$(MKDIR) doc/stdlib/html
+	$(COQDOC) -q -d doc/stdlib/html --multi-index --html -g \
+	  -R theories Coq $(THEORIESVO:.vo=.v)
+	mv doc/stdlib/html/index.html doc/stdlib/index-body.html
+else
 doc/stdlib/index-body.html: | $(COQDOC) $(THEORIESVO)
 	- rm -rf doc/stdlib/html
 	$(MKDIR) doc/stdlib/html
 	$(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g \
 	  -R theories Coq $(THEORIESVO:.vo=.v)
 	mv doc/stdlib/html/index.html doc/stdlib/index-body.html
+endif
 
-doc/stdlib/index-list.html: doc/stdlib/index-list.html.template
+doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index
 	./doc/stdlib/make-library-index doc/stdlib/index-list.html
 
 doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.html doc/stdlib/index-trailer.html
@@ -167,17 +202,26 @@ doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.htm
 
 ### Standard library (light version, full version is definitely too big)
 
+ifeq ($(QUICK),1)
+doc/stdlib/Library.coqdoc.tex:
+	$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
+            -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
+else
 doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO)
 	$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
             -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
+endif
 
 doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
 	(cd doc/stdlib;\
-	$(LATEX) Library;\
-	$(LATEX) Library)
+	$(LATEX) -interaction=batchmode Library;\
+	$(LATEX) -interaction=batchmode Library > /dev/null;\
+	../tools/show_latex_messages Library.log)
 
 doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.dvi
-	(cd doc/stdlib; $(PDFLATEX) Library)
+	(cd doc/stdlib;\
+	$(PDFLATEX) -interaction=batchmode Library;\
+	../tools/show_latex_messages Library.log)
 
 ######################################################################
 # Tutorial on inductive types
@@ -185,13 +229,16 @@ doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Li
 
 doc/RecTutorial/RecTutorial.v.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.tex
 	(cd doc/RecTutorial;\
-	 $(LATEX) RecTutorial.v;\
-	 $(BIBTEX) RecTutorial.v;\
-	 $(LATEX) RecTutorial.v;\
-	 $(LATEX) RecTutorial.v)
+	$(LATEX) -interaction=batchmode RecTutorial.v;\
+	$(BIBTEX) -terse RecTutorial.v;\
+	$(LATEX) -interaction=batchmode RecTutorial.v > /dev/null;\
+	$(LATEX) -interaction=batchmode RecTutorial.v > /dev/null;\
+	../tools/show_latex_messages RecTutorial.v.log)
 
 doc/RecTutorial/RecTutorial.v.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.dvi
-	(cd doc/RecTutorial; $(PDFLATEX) RecTutorial.v.tex)
+	(cd doc/RecTutorial;\
+	$(PDFLATEX) -interaction=batchmode RecTutorial.v.tex;\
+	../tools/show_latex_messages RecTutorial.v.log)
 
 doc/RecTutorial/RecTutorial.v.html: doc/RecTutorial/RecTutorial.v.tex
 	(cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial.v)
diff --git a/checker/check.ml b/checker/check.ml
index 40ac604e0..82df62b4c 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -211,7 +211,7 @@ let locate_absolute_library dir =
   if loadpath = [] then raise LibUnmappedDir;
   try
     let name = string_of_id base^".vo" in
-    let _, file = System.where_in_path false loadpath name in
+    let _, file = System.where_in_path ~warn:false loadpath name in
     (dir, file)
   with Not_found ->
   (* Last chance, removed from the file system but still in memory *)
@@ -231,7 +231,7 @@ let locate_qualified_library qid =
     in
     if loadpath = [] then raise LibUnmappedDir;
     let name =  qid.basename^".vo" in
-    let path, file = System.where_in_path true loadpath name in
+    let path, file = System.where_in_path loadpath name in
     let dir =
       extend_dirpath (find_logical_path path) (id_of_string qid.basename) in
     (* Look if loaded *)
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
+
diff --git a/lib/envars.ml b/lib/envars.ml
index 867297a86..3246c1478 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -20,14 +20,13 @@ let guess_coqlib () =
     then Coq_config.coqlib
     else 
       let prefix = Filename.dirname (Filename.dirname Sys.executable_name) in
-      let coqlib = if Coq_config.local then prefix else 
+      let coqlib = if !Flags.boot || Coq_config.local then prefix else 
 	List.fold_left Filename.concat prefix ["lib";"coq"] in
 	if Sys.file_exists (Filename.concat coqlib file) then coqlib else
 	  Util.error "cannot guess a path for Coq libraries; please use -coqlib option"
 	  
 let coqlib () = 
-  if !Flags.coqlib_spec then !Flags.coqlib else
-    (if !Flags.boot then Coq_config.coqsrc else guess_coqlib ())
+  if !Flags.coqlib_spec then !Flags.coqlib else guess_coqlib ()
 
 let path_to_list p =
   let sep = if Sys.os_type = "Win32" then ';' else ':' in
diff --git a/lib/flags.ml b/lib/flags.ml
index c3033c4b5..c0af148c7 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -13,6 +13,11 @@ let with_option o f x =
   try let r = f x in o := old; r
   with e -> o := old; raise e
 
+let without_option o f x =
+  let old = !o in o:=false;
+  try let r = f x in o := old; r
+  with e -> o := old; raise e
+
 let boot = ref false
 
 let batch_mode = ref false
@@ -44,16 +49,8 @@ let make_silent flag = silent := flag; ()
 let is_silent () = !silent
 let is_verbose () = not !silent
 
-let silently f x =
-  let oldsilent = !silent in
-  try 
-    silent := true;
-    let rslt = f x in
-    silent := oldsilent; 
-    rslt
-  with e -> begin
-    silent := oldsilent; raise e
-  end
+let silently f x = with_option silent f x
+let verbosely f x = without_option silent f x
 
 let if_silent f x = if !silent then f x
 let if_verbose f x = if not !silent then f x
diff --git a/lib/flags.mli b/lib/flags.mli
index f0e4103f6..fe1157d88 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -38,6 +38,7 @@ val make_silent : bool -> unit
 val is_silent : unit -> bool
 val is_verbose : unit -> bool
 val silently : ('a -> 'b) -> 'a -> 'b
+val verbosely : ('a -> 'b) -> 'a -> 'b
 val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
@@ -46,9 +47,13 @@ val if_warn : ('a -> unit) -> 'a -> unit
 
 val hash_cons_proofs : bool ref
 
-(* Temporary activate an option ('c must be an atomic type) *)
+(* Temporary activate an option (to activate option [o] on [f x y z],
+   use [with_option o (f x y) z]) *)
 val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 
+(* Temporary deactivate an option *)
+val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
+
 (* If [None], no limit *)
 val set_print_hyps_limit : int option -> unit
 val print_hyps_limit : unit -> int option
diff --git a/lib/system.ml b/lib/system.ml
index 00d6dec22..2c63b4cc7 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -128,7 +128,7 @@ let all_subdirs ~unix_path:root =
   if exists_dir root then traverse root [];
   List.rev !l
 
-let where_in_path warn path filename =
+let where_in_path ?(warn=true) path filename =
   let rec search = function
     | lpe :: rem ->
 	let f = Filename.concat lpe filename in
@@ -144,26 +144,26 @@ let where_in_path warn path filename =
 	    msg_warning
 	      (str filename ++ str " has been found in" ++ spc () ++
 	       hov 0 (str "[ " ++
-	         hv 0 (prlist_with_sep (fun () -> spc() ++ pr_semicolon())
+	         hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
 		   (fun (lpe,_) -> str lpe) l)
 	         ++ str " ];") ++ fnl () ++
 	       str "loading " ++ str f);
 	  (lpe, f) in
   check_and_warn (search path)
 
-let find_file_in_path paths filename =
+let find_file_in_path ?(warn=true) paths filename =
   if not (Filename.is_implicit filename) then
     let root = Filename.dirname filename in
     root, filename
   else 
-    try where_in_path true paths filename
+    try where_in_path ~warn paths filename
     with Not_found ->
       errorlabstrm "System.find_file_in_path"
 	(hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++ 
 		str "on loadpath"))
 
 let is_in_path lpath filename =
-  try ignore (where_in_path false lpath filename); true
+  try ignore (where_in_path ~warn:false lpath filename); true
   with Not_found -> false
 
 let make_suffix name suffix =
@@ -201,7 +201,7 @@ let raw_extern_intern magic suffix =
   in 
   (extern_state,intern_state)
 
-let extern_intern magic suffix =
+let extern_intern ?(warn=true) magic suffix =
   let (raw_extern,raw_intern) = raw_extern_intern magic suffix in
   let extern_state name val_0 = 
     try
@@ -214,7 +214,7 @@ let extern_intern magic suffix =
     with Sys_error s -> error ("System error: " ^ s)
   and intern_state paths name = 
     try
-      let _,filename = find_file_in_path paths (make_suffix name suffix) in
+      let _,filename = find_file_in_path ~warn paths (make_suffix name suffix) in
       let channel = raw_intern filename in
       let v = marshal_in channel in
       close_in channel; 
diff --git a/lib/system.mli b/lib/system.mli
index 48e02cb5d..7556ed9e4 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -22,7 +22,7 @@ val exclude_search_in_dirname : string -> unit
 
 val all_subdirs : unix_path:string -> (physical_path * string list) list
 val is_in_path : load_path -> string -> bool
-val where_in_path : bool -> load_path -> string -> physical_path * string
+val where_in_path : ?warn:bool -> load_path -> string -> physical_path * string
 
 val physical_path_of_string : string -> physical_path
 val string_of_physical_path : physical_path -> string
@@ -36,7 +36,8 @@ val home : string
 
 val exists_dir : string -> bool
 
-val find_file_in_path : load_path -> string -> physical_path * string
+val find_file_in_path :
+  ?warn:bool -> load_path -> string -> physical_path * string
 
 (*s Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]
@@ -50,8 +51,8 @@ exception Bad_magic_number of string
 val raw_extern_intern : int -> string -> 
   (string -> string * out_channel) * (string -> in_channel)
 
-val extern_intern : 
-  int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a)
+val extern_intern : ?warn:bool -> int -> string -> 
+  (string -> 'a -> unit) * (load_path -> string -> 'a)
 
 (*s Sending/receiving once with external executable *)
 
diff --git a/library/library.ml b/library/library.ml
index ff0e62064..7b20f13bf 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -350,7 +350,7 @@ let locate_absolute_library dir =
   if loadpath = [] then raise LibUnmappedDir;
   try
     let name = (string_of_id base)^".vo" in
-    let _, file = System.where_in_path false loadpath name in
+    let _, file = System.where_in_path ~warn:false loadpath name in
     (dir, file)
   with Not_found ->
   (* Last chance, removed from the file system but still in memory *)
@@ -366,7 +366,7 @@ let locate_qualified_library warn qid =
     let loadpath = loadpaths_matching_dir_path dir in
     if loadpath = [] then raise LibUnmappedDir;
     let name = string_of_id base ^ ".vo" in
-    let lpath, file = System.where_in_path warn (List.map fst loadpath) name in
+    let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in
     let dir = extend_dirpath (List.assoc lpath loadpath) base in
     (* Look if loaded *)
     if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir)
@@ -477,7 +477,9 @@ let rec_intern_by_filename_only id f =
 
 let rec_intern_library_from_file idopt f =
   (* A name is specified, we have to check it contains library id *)
-  let _, f = System.find_file_in_path (get_load_paths ()) (f^".vo") in
+  let paths = get_load_paths () in
+  let _, f = 
+    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in
   rec_intern_by_filename_only idopt f
 
 (**********************************************************************)
@@ -605,7 +607,9 @@ let check_coq_overwriting p =
     errorlabstrm "" (strbrk ("Name "^string_of_dirpath p^" starts with prefix \"Coq\" which is reserved for the Coq library."))
 
 let start_library f = 
-  let _,longf = System.find_file_in_path (get_load_paths ()) (f^".v") in
+  let paths = get_load_paths () in
+  let _,longf =
+    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
   let ldir0 = find_logical_path (Filename.dirname longf) in
   check_coq_overwriting ldir0;
   let id = id_of_string (Filename.basename f) in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index dab5c7987..eb1035f2c 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -493,25 +493,25 @@ let clear_hyps_in_evi evdref hyps concl ids =
    dependencies in variables are canonically associated to the most ancient
    variable in its family of aliased variables *)
 
-let rec expand_var_at_least_once env x = match kind_of_term x with
+let expand_var_once env x = match kind_of_term x with
   | Rel n ->
       begin match pi2 (lookup_rel n env) with
-      | Some t when isRel t or isVar t ->
-	  let t = lift n t in
-	  (try expand_var_at_least_once env t with Not_found -> t)
-      | _ ->
-	  raise Not_found
+      | Some t when isRel t or isVar t -> lift n t
+      | _ -> raise Not_found
       end
   | Var id ->
       begin match pi2 (lookup_named id env) with
-      | Some t when isVar t ->
-	  (try expand_var_at_least_once env t with Not_found -> t)
-      | _ ->
-	  raise Not_found
+      | Some t when isVar t -> t
+      | _ -> raise Not_found
       end
   | _ ->
       raise Not_found
 
+let rec expand_var_at_least_once env x =
+  let t = expand_var_once env x in
+  try expand_var_at_least_once env t
+  with Not_found -> t
+
 let expand_var env x =
   try expand_var_at_least_once env x with Not_found -> x
   
@@ -522,6 +522,13 @@ let rec expand_vars_in_term env t = match kind_of_term t with
   | Rel _ | Var _ -> expand_var env t
   | _ -> map_constr_with_full_binders push_rel expand_vars_in_term env t
 
+let rec expansions_of_var env x =
+  try 
+    let t = expand_var_once env x in
+    t :: expansions_of_var env t
+  with Not_found ->
+    [x]
+
 (* [find_projectable_vars env sigma y subst] finds all vars of [subst]
  * that project on [y]. It is able to find solutions to the following
  * two kinds of problems:
@@ -710,8 +717,8 @@ let do_restrict_hyps_virtual evd evk filter =
          unsolvable.
        Computing whether y is erasable or not may be costly and the 
        interest for this early detection in practice is not obvious. We let
-       it for future work. Anyway, thanks to the use of filters, the whole
-       context remains consistent. *)
+       it for future work. In any case, thanks to the use of filters, the whole
+       (unrestricted) context remains consistent. *)
     let evi = Evd.find (evars_of evd) evk in
     let env = evar_unfiltered_env evi in
     let oldfilter = evar_filter evi in
@@ -853,7 +860,9 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
       | NotUnique ->
 	  if not !progress then raise NotEnoughInformationToProgress;
 	  (* No unique projection but still restrict to where it is possible *)
-	  let filter = array_map_to_list (fun c -> isEvar c or c = t) argsv in
+	  let ts = expansions_of_var env t in
+	  let test c = isEvar c or List.mem c ts in
+	  let filter = array_map_to_list test argsv in
 	  let args' = filter_along (fun x -> x) filter argsv in
 	  let evd,evar = do_restrict_hyps_virtual !evdref evk filter in
 	  let evk',_ = destEvar evar in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index aadb36396..9d99ed6d4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -704,8 +704,8 @@ let plain_instance s c =
      If a lemma has the type "(fun x => p) t" then rewriting t may fail
      if the type of the lemma is first beta-reduced (this typically happens
      when rewriting a single variable and the type of the lemma is obtained
-     by meta_instance (with empty map) which itself call instance with this
-     empty map.
+     by meta_instance (with empty map) which itself calls instance with this
+     empty map).
  *)
 
 let instance s c =
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 83693827c..7755efeb5 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -298,14 +298,23 @@ let rename_hyp id1 id2 sign =
 (* Will only be used on terms given to the Refine rule which have meta 
 variables only in Application and Case *)
 
+let error_unsupported_deep_meta c =
+  errorlabstrm "" (strbrk "Application of lemmas whose beta-iota normal " ++
+    strbrk "form contains metavariables deep inside the term is not " ++
+    strbrk "supported; try \"refine\" instead.")
+
 let collect_meta_variables c = 
-  let rec collrec acc c = match kind_of_term c with
-    | Meta mv -> mv::acc
-    | Cast(c,_,_) -> collrec acc c
-    | (App _| Case _) -> fold_constr collrec acc c
-    | _ -> acc
-  in 
-  List.rev(collrec [] c)
+  let rec collrec deep acc c = match kind_of_term c with
+    | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
+    | Cast(c,_,_) -> collrec deep acc c
+    | (App _| Case _) -> fold_constr (collrec deep) acc c
+    | _ -> fold_constr (collrec true) acc c
+  in
+  List.rev (collrec false [] c)
+
+let check_meta_variables c = 
+  if not (list_distinct (collect_meta_variables c)) then
+    raise (RefinerError (NonLinearProof c))
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check & not (is_conv_leq env sigma ty conclty) then 
@@ -366,6 +375,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     | _ -> 
 	if occur_meta trm then
 	  anomaly "refiner called with a meta in non app/case subterm";
+
       	let t'ty = goal_type_of env sigma trm in
 	check_conv_leq_goal env sigma trm t'ty conclty;
         (goalacc,t'ty)
@@ -563,8 +573,7 @@ let prim_refiner r sigma goal =
 	  (mk_sign sign all, sigma)
 
     | Refine c ->
-        if not (list_distinct (collect_meta_variables c)) then
-          raise (RefinerError (NonLinearProof c));
+	check_meta_variables c;
 	let (sgl,cl') = mk_refgoals sigma goal [] cl c in
 	let sgl = List.rev sgl in
 	  (sgl, sigma)
diff --git a/test-suite/bugs/closed/shouldsucceed/1907.v b/test-suite/bugs/closed/shouldsucceed/1907.v
new file mode 100644
index 000000000..55fc82319
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1907.v
@@ -0,0 +1,7 @@
+(* An example of type inference *)
+
+Axiom A : Type.
+Definition f (x y : A) := x.
+Axiom g : forall x y : A, f x y = y -> Prop.
+Axiom x : A.
+Check (g x _ (refl_equal x)).
diff --git a/test-suite/bugs/closed/shouldsucceed/1925.v b/test-suite/bugs/closed/shouldsucceed/1925.v
new file mode 100644
index 000000000..17eb721ad
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1925.v
@@ -0,0 +1,22 @@
+(* Check that the analysis of projectable rel's in an evar instance is up to
+   aliases *)
+
+Require Import List.
+
+Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C := 
+  fun x : A => g(f x).
+
+Definition map_fuse' : 
+  forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A), 
+    (map g (map f xs)) = map (compose _ _ _ g f) xs 
+    :=
+    fun A B C g f => 
+      (fix loop (ys : list A) {struct ys} :=
+        match ys as ys return (map g (map f ys)) = map (compose _ _ _ g f) ys
+        with
+        | nil => refl_equal nil
+        | x :: xs =>
+           match loop xs in eq _ a return eq _  ((g (f x)) :: a) with
+            | refl_equal => refl_equal (map g (map f (x :: xs)))
+           end
+        end).
diff --git a/test-suite/bugs/closed/shouldsucceed/1944.v b/test-suite/bugs/closed/shouldsucceed/1944.v
new file mode 100644
index 000000000..7d9f9eb26
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1944.v
@@ -0,0 +1,9 @@
+(* Test some uses of ? in introduction patterns *)
+
+Inductive J : nat -> Prop := 
+  | K : forall p, J p -> (True /\ True)  -> J (S p).
+
+Lemma bug : forall n, J n -> J (S n).
+Proof.
+  intros ? H.
+  induction H as [? ? [? ?]].
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 4bdd579a6..d3b368952 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -31,3 +31,8 @@ Notation "' 'C_' G ( A )" := (A,G) (at level 8, G at level 2).
 
 Notation "+1 x" := (S x) (at level 25, x at level 9).
 Section A. Global Notation "'Z'" := O (at level 9). End A.
+
+(* Check use of "$" (see bug #1961) *)
+
+Notation "$ x" := (id x) (at level 30).
+Check ($ 5).
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index a35b6ffa4..d1910c145 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -108,7 +108,8 @@ let dir_ml_load s =
 	 * if this code section starts to use a module not used elsewhere
 	 * in this file, the Makefile dependency logic needs to be updated.
 	 *)
-        let _,gname = where_in_path true !coq_mlpath_copy s in
+        let warn = Flags.is_verbose() in
+        let _,gname = where_in_path ~warn !coq_mlpath_copy s in
         try
           Dynlink.loadfile gname;
 	with | Dynlink.Error a ->
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c7224ddaa..aa519cd8c 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -57,7 +57,9 @@ let real_error = function
    the file we parse seems a bit risky to me.  B.B.  *)
 
 let open_file_twice_if verbosely fname =
-  let _,longfname = find_file_in_path (Library.get_load_paths ()) fname in
+  let paths = Library.get_load_paths () in
+  let _,longfname =
+    find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
   let in_chan = open_in longfname in
   let verb_ch = if verbosely then Some (open_in longfname) else None in
   let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
@@ -131,7 +133,8 @@ let rec vernac_com interpfun (loc,com) =
         let cds = Dumpglob.coqdoc_freeze() in
           if !Flags.beautify_file then 
 	    begin
-              let _,f = find_file_in_path (Library.get_load_paths ())
+              let _,f = find_file_in_path ~warn:(Flags.is_verbose())
+		(Library.get_load_paths ())
 		(make_suffix fname ".v") in
 		chan_beautify := open_out (f^beautify_suffix);
 		Pp.comments := []
@@ -227,7 +230,7 @@ let load_vernac verb file =
 
 (* Compile a vernac file (f is assumed without .v suffix) *)
 let compile verbosely f =
-  let ldir,long_f_dot_v = Library.start_library f in
+  let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
     if Dumpglob.multi_dump () then 
       Dumpglob.open_glob_file (f ^ ".glob");
     Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ab3df8c0c..39a545215 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -235,7 +235,7 @@ let dump_universes s =
 
 let locate_file f =
   try
-    let _,file = System.where_in_path false (Library.get_load_paths ()) f in
+    let _,file = System.where_in_path ~warn:false (Library.get_load_paths ()) f in
     msgnl (str file)
   with Not_found -> 
     msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
@@ -592,11 +592,10 @@ let vernac_end_segment lid =
 
 let vernac_require import _ qidl =
   let qidl = List.map qualid_of_reference qidl in
-  let modrefl = List.map Library.try_locate_qualified_library qidl in
-(*   let modrefl = List.map (fun qid -> let (dp, _) = (Library.try_locate_qualified_library qid) in dp) qidl in *)
-    if Dumpglob.dump () then
-      List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl);
-    Library.require_library_from_dirpath modrefl import
+  let modrefl = Flags.silently (List.map Library.try_locate_qualified_library) qidl in
+  if Dumpglob.dump () then
+    List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl);
+  Library.require_library_from_dirpath modrefl import
 
 let vernac_canonical r =
   Recordops.declare_canonical_structure (global_with_alias r)