7 files changed, 13 insertions, 14 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 4309926b9..baf3d4991 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -1983,7 +1983,7 @@ todo
 
 \Question{Can you show me an example of a tactic written in OCaml?}
 
-You have some examples of tactics written in Ocaml in the ``contrib'' directory of {\Coq} sources. 
+You have some examples of tactics written in Ocaml in the ``plugins'' directory of {\Coq} sources. 
 
 
 
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index ba07182a6..8271c7c32 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -620,7 +620,7 @@ quite efficient for Caml code.
 As a test, we propose an automatic extraction of the 
 Standard Library of \Coq. In particular, we will find back the
 two previous examples, {\tt Euclid} and {\tt Heapsort}. 
-Go to directory {\tt contrib/extraction/test} of the sources of \Coq,
+Go to directory {\tt plugins/extraction/test} of the sources of \Coq,
 and run commands: 
 \begin{verbatim}
 make tree; make
@@ -653,7 +653,7 @@ also work, just adapt the {\tt Makefile.haskell}. In particular {\tt
 
 Some pathological examples of extraction are grouped in the file
 \begin{verbatim}
-contrib/extraction/test_extraction.v
+plugins/extraction/test_extraction.v
 \end{verbatim}
 of the sources of \Coq.
 
diff --git a/doc/refman/Helm.tex b/doc/refman/Helm.tex
index d07b1204c..74db9c86d 100644
--- a/doc/refman/Helm.tex
+++ b/doc/refman/Helm.tex
@@ -273,7 +273,7 @@ of the calculus is also proved.
 \subsubsection{The CIC with Explicit Named Substitutions XML DTD}
  
 A copy of the DTD can be found in the file ``\verb+cic.dtd+'' in the
-\verb+contrib/xml+ source directory of \Coq.
+\verb+plugins/xml+ source directory of \Coq.
 The following is a very brief overview of the elements described in the DTD.
  
 \begin{description}
diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
index 48937113f..94c76c197 100644
--- a/doc/refman/Polynom.tex
+++ b/doc/refman/Polynom.tex
@@ -336,21 +336,21 @@ describes their syntax and effects:
   evaluation function of power coefficient) is the original term, or
   returns {\tt InitialRing.NotConstant} if not a constant coefficient
   (i.e. {\ltac} is the inverse function of {\tt Cp\_phi}).
-  See files {\tt contrib/setoid\_ring/ZArithRing.v} and
-  {\tt contrib/setoid\_ring/RealField.v} for examples.
+  See files {\tt plugins/setoid\_ring/ZArithRing.v} and
+  {\tt plugins/setoid\_ring/RealField.v} for examples.
   By default the tactic does not recognize power expressions as ring
   expressions.
 \item[sign {\term}] allows {\tt ring\_simplify} to use a minus operation
   when outputing its normal form, i.e writing $x - y$ instead of $x + (-y)$. 
   The term {\term} is a proof that a given sign function indicates expressions
    that are signed ({\term} has to be a
-  proof of {\tt Ring\_theory.get\_sign}). See  {\tt contrib/setoid\_ring/IntialRing.v} for examples of sign function.
+  proof of {\tt Ring\_theory.get\_sign}). See  {\tt plugins/setoid\_ring/IntialRing.v} for examples of sign function.
 \item[div {\term}] allows  {\tt ring} and {\tt ring\_simplify} to use moniomals
 with coefficient other than 1 in the rewriting. The term {\term} is a proof that a given division function  satisfies the specification of an euclidean
   division function  ({\term} has to be a
   proof of {\tt Ring\_theory.div\_theory}). For example, this function is
   called when trying to rewrite $7x$ by $2x = z$ to tell that $7 = 3 * 2 + 1$.
-   See  {\tt contrib/setoid\_ring/IntialRing.v} for examples of div function.
+   See  {\tt plugins/setoid\_ring/IntialRing.v} for examples of div function.
   
 \end{description}
 
@@ -490,7 +490,7 @@ constants can be proven different from zero automatically.
 The tactic must be loaded by \texttt{Require Import Field}. New field
 structures can be declared to the system with the \texttt{Add Field}
 command (see below). The field of real numbers is defined in module
-\texttt{RealField} (in texttt{contrib/setoid\_ring}). It is exported
+\texttt{RealField} (in texttt{plugins/setoid\_ring}). It is exported
 by module \texttt{Rbase}, so that requiring \texttt{Rbase} or
 \texttt{Reals} is enough to use the field tactics on real
 numbers. Rational numbers in canonical form are also declared as a
@@ -696,7 +696,7 @@ the file
 
 \begin{quotation}
 \begin{verbatim}
-contrib/ring/Ring_theory.v
+plugins/ring/Ring_theory.v
 \end{verbatim}
 \end{quotation}
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9ed2e650c..4e31137c9 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3565,7 +3565,7 @@ intros; field.
 Reset Initial.
 \end{coq_eval}
 
-\SeeAlso file {\tt contrib/setoid\_ring/RealField.v} for an example of instantiation,\\
+\SeeAlso file {\tt plugins/setoid\_ring/RealField.v} for an example of instantiation,\\
 \phantom{\SeeAlso}theory {\tt theories/Reals} for many examples of use of {\tt
 field}.
 
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index dbd863469..9af44115a 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -1084,7 +1084,7 @@ is undecidable in general case, don't expect miracles from it!
 
 % \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v}
 
-\SeeAlso comments of source file \texttt{tactics/contrib/polynom/quote.ml}
+\SeeAlso comments of source file \texttt{plugins/quote/quote.ml}
 
 \SeeAlso the \texttt{ring} tactic (Chapter~\ref{ring})
 
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
index d7239c8fd..5a3ccda6a 100644
--- a/doc/refman/RefMan-tus.tex
+++ b/doc/refman/RefMan-tus.tex
@@ -1186,8 +1186,7 @@ function body or behind the \texttt{lazy} keyword.
 
 One can see examples of that technique in the source code of \Coq{},
 for example 
-\verb+tactics/contrib/polynom/ring.ml+ or 
-\verb+tactics/contrib/polynom/coq_omega.ml+.
+\verb+plugins/omega/coq_omega.ml+.
 
 \section[Some Useful Tools for Writing Tactics]{Some Useful Tools for Writing Tactics\label{SomeUsefulToolsforWrittingTactics}}
 When the implementation of a tactic is not a straightforward