301 files changed, 169 insertions, 170 deletions

diff --git a/CHANGES b/CHANGES
index df2783349..dc7efbab3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1023,7 +1023,7 @@ Tactics
 - Clear now fails when trying to remove a local definition used by
   a constant appearing in the current goal
 
-Extraction (See details in contrib/extraction/CHANGES)
+Extraction (See details in plugins/extraction/CHANGES)
 
 - The old commands: 	(Recursive) Extraction Module M.
   are now:              (Recursive) Extraction Library M. 
@@ -1163,7 +1163,7 @@ Tactics
 - Unfold expects a correct evaluable argument
 - Clear expects existing hypotheses
 
-Extraction (See details in contrib/extraction/CHANGES and README):
+Extraction (See details in plugins/extraction/CHANGES and README):
 
 - An experimental Scheme extraction is provided.
 - Concerning Ocaml, extracted code is now ensured to always type-check, 
@@ -1278,7 +1278,7 @@ Bugs
 - Known bugs related to Inversion and let-in's fixed
 - Bug unexpected Delta with let-in now fixed
 
-Extraction (details in contrib/extraction/CHANGES or documentation)
+Extraction (details in plugins/extraction/CHANGES or documentation)
 
 - Signatures of extracted terms are now mostly expunged from dummy arguments.
 - Haskell extraction is now operational (tested & debugged).  
@@ -1286,7 +1286,7 @@ Extraction (details in contrib/extraction/CHANGES or documentation)
 Standard library
 
 - Some additions in [ZArith]: three files (Zcomplements.v, Zpower.v
-  and Zlogarithms.v) moved from contrib/omega in order to be more
+  and Zlogarithms.v) moved from plugins/omega in order to be more
   visible, one Zsgn function, more induction principles (Wf_Z.v and
   tail of Zcomplements.v), one more general Euclid theorem
 - Peano_dec.v and Compare_dec.v now part of Arith.v
@@ -1349,7 +1349,7 @@ Tactics
 - Slight improvement in naming strategy for NewInduction/NewDestruct
 - Intuition/Tauto do not perform useless unfolding and work up to conversion
 
-Extraction (details in contrib/extraction/CHANGES or documentation)
+Extraction (details in plugins/extraction/CHANGES or documentation)
 
 - Syntax changes: there are no more options inside the extraction commands. 
   New commands for customization and options have been introduced instead. 
diff --git a/COPYRIGHT b/COPYRIGHT
index 7ed31f15d..63d905739 100644
--- a/COPYRIGHT
+++ b/COPYRIGHT
@@ -13,12 +13,12 @@ work time rest with the employee. By analogy, it is Lionel's opinion
 that copyright on these changes rests with him.
 
 This product includes also software developed by
-	Yves Bertot, Lemme, INRIA Sophia-Antipolis (contrib/interface,
+	Yves Bertot, Lemme, INRIA Sophia-Antipolis (plugins/interface,
 parsing/search.ml)
-	Pierre Crégut, France Telecom R & D (contrib/omega and contrib/romega)
-	Pierre Courtieu, Lemme (contrib/funind)
-	Loïc Pottier, Lemme, INRIA Sophia-Antipolis (contrib/fourier)
-	Claudio Sacerdoti Coen, HELM, University of Bologna, (contrib/xml)
+	Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega)
+	Pierre Courtieu, Lemme (plugins/funind)
+	Loïc Pottier, Lemme, INRIA Sophia-Antipolis (plugins/fourier)
+	Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml)
 
 The file CREDITS contains a list of past contributors
 The credits section in Reference Manual introduction details
diff --git a/CREDITS b/CREDITS
index b3d563caf..c982d6724 100644
--- a/CREDITS
+++ b/CREDITS
@@ -23,53 +23,53 @@ The following directories contain independent contributions supported
 by the Coq development team. All of them are released under the terms of
 the GNU Lesser General Public License Version 2.1.
 
-contrib/cc
+plugins/cc
   developed by Pierre Corbineau (ENS Cachan, 2001, LRI, 2001-2005, Radboud
   University at Nijmegen, 2005-2008)
-contrib/correctness
+plugins/correctness
   developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
-contrib/dp
+plugins/dp
   developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre
   (LRI, 2005-2008)
-contrib/extraction
+plugins/extraction
   developed by Pierre Letouzey (LRI, 2000-2004, PPS-Paris7, 2005-now)
-contrib/field
+plugins/field
   developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
-contrib/firstorder 
+plugins/firstorder 
   developed by Pierre Corbineau (LRI, 2003-2008)
-contrib/fourier
+plugins/fourier
   developed by Loïc Pottier (INRIA-Lemme, 2001)
-contrib/funind
+plugins/funind
   developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2008),
   Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008) 
   and Yves Bertot (INRIA-Marelle, 2005-2006)
-contrib/interface
+plugins/interface
   developed by Yves Bertot with contributions from Loïc Pottier and
   Laurence Rideau as part of the Pcoq project (INRIA-Lemme, 1997-2006);
   extended by Lionel Mamane as part of the TeXMacs project (Radboud university
   at Nijmegen, 2007-2008)
-contrib/omega
+plugins/omega
   developed by Pierre Crégut (France Telecom R&D, 1996)
-contrib/recdef
+plugins/recdef
   developed by Yves Bertot (INRIA-Marelle, 2005-2006)
-contrib/ring
+plugins/ring
   developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick 
   Loiseleur (LRI, 1997-1999)
-contrib/romega
+plugins/romega
   developed by Pierre Crégut (France Telecom R&D, 2001-2004)
-contrib/rtauto
+plugins/rtauto
   developed by Pierre Corbineau (LRI, 2005)
-contrib/setoid_ring
+plugins/setoid_ring
   developed by Benjamin Grégoire (INRIA-Everest, 2005-2006), 
   Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006) 
   and Bruno Barras (INRIA LogiCal, 2005-2006),
-contrib/subtac
+plugins/subtac
   developed by Matthieu Sozeau (LRI, 2005-2008)
-contrib/xml
+plugins/xml
   developed by Claudio Sacerdoti (Univ. Bologna, 2000-2005) 
   as part of the HELM and MoWGLI projects; extension by Cezary Kaliszyk as
   part of the ProofWeb project (Radbout University at Nijmegen, 2008)
-contrib/micromega
+plugins/micromega
   developed by Frédéric Besson (IRISA/INRIA, 2006-2008), with some 
   extensions by Evgeny Makarov (INRIA, 2007); sum-of-squares solver and 
   interface to the csdp solver uses code from John Harrison (University
diff --git a/Makefile b/Makefile
index 1413d0faa..e8f5fabfe 100644
--- a/Makefile
+++ b/Makefile
@@ -196,8 +196,8 @@ indepclean:
 	rm -f bin/coq-interface$(EXE) bin/coq-parser$(EXE)
 	find . -name '*~' -or -name '*.cm[ioa]' | xargs rm -f
 	find . -name '*_mod.ml' | xargs rm -f
-	find contrib test-suite -name '*.vo' -or -name '*.glob' | xargs rm -f
-	rm -f */*.pp[iox] contrib/*/*.pp[iox]
+	find plugins test-suite -name '*.vo' -or -name '*.glob' | xargs rm -f
+	rm -f */*.pp[iox] plugins/*/*.pp[iox]
 	rm -rf $(SOURCEDOCDIR)
 	rm -f toplevel/mltop.byteml toplevel/mltop.optml
 	rm -f test-suite/check.log
diff --git a/Makefile.build b/Makefile.build
index a3298230c..dd27cfcbd 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -156,7 +156,7 @@ coqbinaries:: ${COQBINARIES} ${CSDPCERT}
 
 coq: coqlib tools coqbinaries
 
-coqlib:: theories contrib
+coqlib:: theories plugins
 
 coqlight: theories-light tools coqbinaries
 
@@ -278,11 +278,11 @@ parsing/highparsing.cmxa: $(HIGHPARSING:.cmo=.cmx)
 tactics/hightactics.cma: $(HIGHTACTICS)
 tactics/hightactics.cmxa: $(HIGHTACTICS:.cmo=.cmx)
 
-contrib/%.cma: | contrib/%.mllib.d
+plugins/%.cma: | plugins/%.mllib.d
 	$(SHOW)'OCAMLC -a -o $@'
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^
 
-contrib/%.cmxa: | contrib/%.mllib.d
+plugins/%.cmxa: | plugins/%.mllib.d
 	$(SHOW)'OCAMLOPT -a -o $@'
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^
 
@@ -309,12 +309,12 @@ checker/check.cmxa: $(MCHECKER:.cmo=.cmx)
 ###########################################################################
 
 ifeq ($(BEST),opt)
-contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMX)
+plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMX)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa -o $@ $^
 	$(STRIP) $@
 else
-contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMO)
+plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO)
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma -o $@ $^
 endif
@@ -453,8 +453,8 @@ install-pcoq-binaries::
 	$(INSTALLBIN) $(COQINTERFACE) $(FULLBINDIR)
 
 install-pcoq-files::
-	$(MKDIR) $(FULLCOQLIB)/contrib/interface
-	$(INSTALLLIB) $(PCOQFILES) $(FULLCOQLIB)/contrib/interface
+	$(MKDIR) $(FULLCOQLIB)/plugins/interface
+	$(INSTALLLIB) $(PCOQFILES) $(FULLCOQLIB)/plugins/interface
 
 install-pcoq-manpages:
 	$(MKDIR) $(FULLMANDIR)/man1
@@ -467,7 +467,7 @@ install-pcoq-manpages:
 VALIDOPTS=-silent -o -m
 
 validate:: $(BESTCHICKEN) $(ALLVO)
-	$(SHOW)'COQCHK <theories & contrib>'
+	$(SHOW)'COQCHK <theories & plugins>'
 	$(HIDE)$(BESTCHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
 
 check:: world validate
@@ -476,7 +476,7 @@ check:: world validate
 	if grep -F 'Error!' test-suite/check.log ; then false; fi
 
 ###########################################################################
-# theories and contrib files
+# theories and plugins files
 ###########################################################################
 
 init: $(INITVO)
@@ -512,10 +512,10 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \
 	wellfounded setoids sorting
 
 ###########################################################################
-# contribs (interface not included)
+# plugins (interface not included)
 ###########################################################################
 
-contrib: $(CONTRIBVO)
+plugins: $(PLUGINSVO)
 omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
 micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT)
 ring: $(RINGVO) $(RINGCMA)
@@ -531,7 +531,7 @@ subtac: $(SUBTACCMA)
 rtauto: $(RTAUTOVO) $(RTAUTOCMA)
 
 ###########################################################################
-# rules to make theories, contrib and states
+# rules to make theories, plugins and states
 ###########################################################################
 
 states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_STRICT) | states/MakeInitial.v.d $(VO_TOOLS_ORDER_ONLY)
@@ -690,8 +690,8 @@ ifeq ($(BEST),opt)
 endif
 # csdpcert is not meant to be directly called by the user; we install
 # it with libraries
-	-$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega
-	$(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/contrib/micromega
+	-$(MKDIR) -p $(FULLCOQLIB)/plugins/micromega
+	$(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/plugins/micromega
 	-$(INSTALLLIB) revision $(FULLCOQLIB)
 
 install-library-light:
diff --git a/Makefile.common b/Makefile.common
index 0fc205b2d..b8462539d 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -58,14 +58,14 @@ COQBINARIES:= $(COQMKTOP) $(COQC) \
 endif
 OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)
 
-CSDPCERT:=contrib/micromega/csdpcert$(EXE)
+CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 
 SRCDIRS:=\
   config 	tools 		tools/coqdoc 	scripts		lib \
   kernel	kernel/byterun	library 	proofs 		tactics \
   pretyping	interp		toplevel 	parsing 	ide/utils \
   ide		\
-  $(addprefix contrib/, \
+  $(addprefix plugins/, \
     omega	romega 		micromega 	quote		ring	dp \
     setoid_ring xml 		extraction 	interface 	fourier \
     cc 		funind 		firstorder 	field 		subtac \
@@ -241,44 +241,44 @@ HIGHTACTICS:=$(addprefix tactics/, \
   eauto.cmo 	class_tactics.cmo	 tauto.cmo \
   eqdecide.cmo )
 
-# NB: Dependencies of contribs are now in separate files
-#  contrib/*/*_plugin.mllib
+# NB: Dependencies of plugins are now in separate files
+#  plugins/*/*_plugin.mllib
 # Format of these files are compatible with ocamlbuild,
 # Even if we don't use it (yet ?)
 
-OMEGACMA:=contrib/omega/omega_plugin.cma
-ROMEGACMA:=contrib/romega/romega_plugin.cma
-MICROMEGACMA:=contrib/micromega/micromega_plugin.cma
-QUOTECMA:=contrib/quote/quote_plugin.cma
-RINGCMA:=contrib/ring/ring_plugin.cma
-NEWRINGCMA:=contrib/setoid_ring/newring_plugin.cma
-GBCMA:=contrib/groebner/groebner_plugin.cma
-DPCMA:=contrib/dp/dp_plugin.cma
-FIELDCMA:=contrib/field/field_plugin.cma
-XMLCMA:=contrib/xml/xml_plugin.cma
-FOURIERCMA:=contrib/fourier/fourier_plugin.cma
-EXTRACTIONCMA:=contrib/extraction/extraction_plugin.cma
-FUNINDCMA:=contrib/funind/recdef_plugin.cma
-FOCMA:=contrib/firstorder/ground_plugin.cma
-CCCMA:=contrib/cc/cc_plugin.cma
-SUBTACCMA:=contrib/subtac/subtac_plugin.cma
-RTAUTOCMA:=contrib/rtauto/rtauto_plugin.cma
-
-CONTRIBS:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \
+OMEGACMA:=plugins/omega/omega_plugin.cma
+ROMEGACMA:=plugins/romega/romega_plugin.cma
+MICROMEGACMA:=plugins/micromega/micromega_plugin.cma
+QUOTECMA:=plugins/quote/quote_plugin.cma
+RINGCMA:=plugins/ring/ring_plugin.cma
+NEWRINGCMA:=plugins/setoid_ring/newring_plugin.cma
+GBCMA:=plugins/groebner/groebner_plugin.cma
+DPCMA:=plugins/dp/dp_plugin.cma
+FIELDCMA:=plugins/field/field_plugin.cma
+XMLCMA:=plugins/xml/xml_plugin.cma
+FOURIERCMA:=plugins/fourier/fourier_plugin.cma
+EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cma
+FUNINDCMA:=plugins/funind/recdef_plugin.cma
+FOCMA:=plugins/firstorder/ground_plugin.cma
+CCCMA:=plugins/cc/cc_plugin.cma
+SUBTACCMA:=plugins/subtac/subtac_plugin.cma
+RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma
+
+PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \
         $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \
         $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \
         $(CCCMA)  $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \
         $(FUNINDCMA) $(GBCMA)
 
 ifneq ($(HASNATDYNLINK),false)
- CONTRIBSTATIC:=
+ STATICPLUGINS:=
  INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \
 	$(XMLCMA) $(FUNINDCMA) $(SUBTACCMA)
  INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
- PLUGINS:=$(CONTRIBS)
- PLUGINSOPT:=$(PLUGINS:.cma=.cmxs)
+ PLUGINS:=$(PLUGINSCMA)
+ PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
 else
- CONTRIBSTATIC:=$(CONTRIBS)
+ STATICPLUGINS:=$(PLUGINSCMA)
  INITPLUGINS:=
  INITPLUGINSOPT:=
  PLUGINS:=
@@ -296,7 +296,7 @@ CMXA:=$(CMA:.cma=.cmxa)
 LINKCMO:=$(CONFIG) lib/lib.cma kernel/kernel.cma library/library.cma \
         pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
         parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \
-        parsing/highparsing.cma tactics/hightactics.cma $(CONTRIBSTATIC)
+        parsing/highparsing.cma tactics/hightactics.cma $(STATICPLUGINS)
 LINKCMX:=$(patsubst %.cma,%.cmxa,$(patsubst %.cmo,%.cmx,$(LINKCMO)))
 
 # objects known by the toplevel of Coq
@@ -332,17 +332,17 @@ COQCCMX:=$(COQCCMO:.cmo=.cmx)
 
 COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-parser$(EXE)
 
-INTERFACECMA:=contrib/interface/coqinterface_plugin.cma
-PARSERCMA:=contrib/interface/coqparser_plugin.cma
+INTERFACECMA:=plugins/interface/coqinterface_plugin.cma
+PARSERCMA:=plugins/interface/coqparser_plugin.cma
 
 ifeq ($(HASNATDYNLINK),false)
  ifeq ($(BEST),opt)
   COQINTERFACE:=$(COQINTERFACE) bin/coq-interface.opt$(EXE) bin/coq-parser.opt$(EXE)
  endif
- INTERFACERC:= contrib/interface/vernacrc
+ INTERFACERC:= plugins/interface/vernacrc
  PCOQPLUGINS:=
 else
- INTERFACERC:= contrib/interface/vernacrc contrib/interface/CoqParser.v
+ INTERFACERC:= plugins/interface/vernacrc plugins/interface/CoqParser.v
  PCOQPLUGINS:=$(INTERFACECMA) $(PARSERCMA)
 endif
 
@@ -351,7 +351,7 @@ PARSERREQUIRESCMX:=$(LINKCMX) $(PARSERCMA:.cma=.cmxa)
 
 ## Misc
 
-CSDPCERTCMO:=$(addprefix contrib/micromega/, \
+CSDPCERTCMO:=$(addprefix plugins/micromega/, \
   mutils.cmo 	micromega.cmo 	mfourier.cmo 	certificate.cmo \
   sos.cmo 	csdpcert.cmo )
 CSDPCERTCMX:= $(CSDPCERTCMO:.cmo=.cmx)
@@ -687,15 +687,15 @@ THEORIESVO:=\
 
 THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO)
 
-## Contribs
+## Plugins
 
-OMEGAVO:=$(addprefix contrib/omega/, \
+OMEGAVO:=$(addprefix plugins/omega/, \
  PreOmega.vo	OmegaLemmas.vo 	OmegaPlugin.vo Omega.vo )
 
-ROMEGAVO:=$(addprefix contrib/romega/, \
+ROMEGAVO:=$(addprefix plugins/romega/, \
  ReflOmegaCore.vo 	ROmega.vo )
 
-MICROMEGAVO:=$(addprefix contrib/micromega/, \
+MICROMEGAVO:=$(addprefix plugins/micromega/, \
   CheckerMaker.vo       Refl.vo \
   Env.vo                RingMicromega.vo \
   EnvRing.vo            VarMap.vo \
@@ -704,10 +704,10 @@ MICROMEGAVO:=$(addprefix contrib/micromega/, \
   QMicromega.vo         RMicromega.vo \
   Tauto.vo )
 
-QUOTEVO:=$(addprefix contrib/quote/, \
+QUOTEVO:=$(addprefix plugins/quote/, \
  Quote.vo )
 
-RINGVO:=$(addprefix contrib/ring/, \
+RINGVO:=$(addprefix plugins/ring/, \
  LegacyArithRing.vo	Ring_normalize.vo \
  LegacyRing_theory.vo	LegacyRing.vo \
  LegacyNArithRing.vo    \
@@ -715,11 +715,11 @@ RINGVO:=$(addprefix contrib/ring/, \
  Setoid_ring_normalize.vo \
  Setoid_ring.vo		Setoid_ring_theory.vo )
 
-FIELDVO:=$(addprefix contrib/field/, \
+FIELDVO:=$(addprefix plugins/field/, \
  LegacyField_Compl.vo   LegacyField_Theory.vo \
  LegacyField_Tactic.vo  LegacyField.vo )
 
-NEWRINGVO:=$(addprefix contrib/setoid_ring/, \
+NEWRINGVO:=$(addprefix plugins/setoid_ring/, \
  BinList.vo   		Ring_theory.vo \
  Ring_polynom.vo	Ring_tac.vo \
  Ring_base.vo 		InitialRing.vo \
@@ -729,48 +729,48 @@ NEWRINGVO:=$(addprefix contrib/setoid_ring/, \
  Field_theory.vo	Field_tac.vo \
  Field.vo		RealField.vo )
 
-GBVO:=$(addprefix contrib/groebner/, \
+GBVO:=$(addprefix plugins/groebner/, \
  GroebnerR.vo		GroebnerZ.vo )
 
 XMLVO:= 
 
-FOURIERVO:=$(addprefix contrib/fourier/, \
+FOURIERVO:=$(addprefix plugins/fourier/, \
  Fourier_util.vo    	Fourier.vo )
 
 FUNINDVO:= 
 
-RECDEFVO:=$(addprefix contrib/funind/, \
+RECDEFVO:=$(addprefix plugins/funind/, \
  Recdef.vo )
 
 CCVO:=
 
-DPVO:=$(addprefix contrib/dp/, \
+DPVO:=$(addprefix plugins/dp/, \
  Dp.vo )
 
-RTAUTOVO:=$(addprefix contrib/rtauto/, \
+RTAUTOVO:=$(addprefix plugins/rtauto/, \
  Bintree.vo	Rtauto.vo )
 
 ifneq ($(HASNATDYNLINK),false)
-INTERFACEVO:=contrib/interface/CoqInterface.vo
+INTERFACEVO:=plugins/interface/CoqInterface.vo
 else
 INTERFACEVO:=
 endif
 
-CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
+PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
 	    $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \
 	    $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \
             $(INTERFACEVO) $(GBVO)
 
-ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO)
+ALLVO:= $(INITVO) $(THEORIESVO) $(PLUGINSVO)
 VFILES:= $(ALLVO:.vo=.v)
 
 # convert a (stdlib) filename into a module name:
-# remove .vo, replace theories and contrib by Coq, and replace slashes by dots
-vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst contrib/%,Coq.%,$(1:.vo=))))
+# remove .vo, replace theories and plugins by Coq, and replace slashes by dots
+vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
 
 ALLMODS:=$(call vo_to_mod,$(ALLVO))
 
-LIBFILES:=$(THEORIESVO) $(CONTRIBVO)
+LIBFILES:=$(THEORIESVO) $(PLUGINSVO)
 LIBFILESLIGHT:=$(THEORIESLIGHTVO)
 
 ## Specials
@@ -839,7 +839,7 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
   pcoq-binaries $(COQINTERFACE) $(CSDPCERT) coqbinaries pcoq $(TOOLS) tools \
   printers debug initplugins plugins \
   world install coqide coqide-files coq coqlib \
-  coqlight states pcoq-files check init theories theories-light contrib \
+  coqlight states pcoq-files check init theories theories-light \
   $(DOC_TARGETS) $(VO_TARGETS) validate \
   %.vo %.glob states/% install-% %.ml4-preprocessed
 
diff --git a/Makefile.doc b/Makefile.doc
index cf849dadf..e5822eb5b 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -49,7 +49,7 @@ ifdef QUICK
 %.v.tex: %.tex
 	(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
 else
-%.v.tex: %.tex | $(COQTEX) $(COQTOPEXE) $(CONTRIBVO) $(THEORIESVO)
+%.v.tex: %.tex | $(COQTEX) $(COQTOPEXE) $(PLUGINSVO) $(THEORIESVO)
 	(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
 endif
 
diff --git a/checker/checker.ml b/checker/checker.ml
index 70e2eb97f..b982456aa 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -113,12 +113,12 @@ let set_rec_include d p =
 let init_load_path () =
   let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
-  let contrib = coqlib/"contrib" in
+  let plugins = coqlib/"plugins" in
   (* first user-contrib *)
   if Sys.file_exists user_contrib then 
     add_rec_path user_contrib Check.default_root_prefix;
-  (* then contrib *)
-  add_rec_path contrib (Names.make_dirpath [coq_root]);
+  (* then plugins *)
+  add_rec_path plugins (Names.make_dirpath [coq_root]);
   (* then standard library *)
 (*  List.iter 
     (fun (s,alias) ->
diff --git a/config/coq_config.mli b/config/coq_config.mli
index b5ccbbca7..7c80a96d4 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -36,7 +36,7 @@ val vo_magic_number : int
 val state_magic_number : int
 
 val theories_dirs : string list
-val contrib_dirs : string list
+val plugins_dirs : string list
 
 val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
 val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof with Coqide *)
diff --git a/configure b/configure
index de3c6fbbd..1e9dc472f 100755
--- a/configure
+++ b/configure
@@ -972,8 +972,8 @@ echo "let theories_dirs = [" >> "$mlconfig_file"
 subdirs theories
 echo "]" >> "$mlconfig_file"
 
-echo "let contrib_dirs = [" >> "$mlconfig_file"
-subdirs contrib
+echo "let plugins_dirs = [" >> "$mlconfig_file"
+subdirs plugins
 echo "]" >> "$mlconfig_file"
 
 chmod a-w "$mlconfig_file"
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 5aadfa592..a9673664a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -344,7 +344,7 @@ Proof_type: subproof field in type proof_tree glued with the ref field
 
 Tacmach: no more echo from functions of module Refiner
 
-Files contrib/*/g_*.ml4 take the place of files contrib/*/*.v.
+Files plugins/*/g_*.ml4 take the place of files plugins/*/*.v.
 Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd
   VERNAC COMMAND EXTEND macros
 File syntax/PPTactic.v moved to parsing/pptactic.ml
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 560d06d96..2598d6df1 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -17,13 +17,13 @@ exec $OCAMLDEBUG \
 	-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
         -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
-        -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \
-        -I $COQTOP/contrib/fourier    -I $COQTOP/contrib/firstorder \
-        -I $COQTOP/contrib/interface \
-        -I $COQTOP/contrib/omega      -I $COQTOP/contrib/romega \
-        -I $COQTOP/contrib/ring       -I $COQTOP/contrib/xml \
-	-I $COQTOP/contrib/subtac     -I $COQTOP/contrib/funind \
-        -I $COQTOP/contrib/rtauto     -I $COQTOP/contrib/setoid_ring \
-        -I $COQTOP/contrib/recdef     -I $COQTOP/contrib/dp \
+        -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
+        -I $COQTOP/plugins/fourier    -I $COQTOP/plugins/firstorder \
+        -I $COQTOP/plugins/interface \
+        -I $COQTOP/plugins/omega      -I $COQTOP/plugins/romega \
+        -I $COQTOP/plugins/ring       -I $COQTOP/plugins/xml \
+	-I $COQTOP/plugins/subtac     -I $COQTOP/plugins/funind \
+        -I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
+        -I $COQTOP/plugins/recdef     -I $COQTOP/plugins/dp \
         -I $COQTOP/ide \
 	$*
diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile
index f2c625ed4..8ad226da6 100644
--- a/dev/ocamlweb-doc/Makefile
+++ b/dev/ocamlweb-doc/Makefile
@@ -4,14 +4,14 @@ LOCALINCLUDES=-I ../../config -I ../../tools -I ../../tools/coqdoc \
 	      -I ../../scripts -I ../../lib -I ../../kernel -I ../../kernel/byterun -I ../../library \
               -I ../../proofs -I ../../tactics -I ../../pretyping \
               -I ../../interp -I ../../toplevel -I ../../parsing -I ../../ide/utils -I ../../ide \
-              -I ../../contrib/omega -I ../../contrib/romega \
-	      -I ../../contrib/ring -I ../../contrib/dp -I ../../contrib/setoid_ring \
-              -I ../../contrib/xml -I ../../contrib/extraction \
-              -I ../../contrib/interface -I ../../contrib/fourier \
-	      -I ../../contrib/cc \
-	      -I ../../contrib/funind -I ../../contrib/firstorder \
-              -I ../../contrib/field -I ../../contrib/subtac -I ../../contrib/rtauto \
-              -I ../../contrib/recdef
+              -I ../../plugins/omega -I ../../plugins/romega \
+	      -I ../../plugins/ring -I ../../plugins/dp -I ../../plugins/setoid_ring \
+              -I ../../plugins/xml -I ../../plugins/extraction \
+              -I ../../plugins/interface -I ../../plugins/fourier \
+	      -I ../../plugins/cc \
+	      -I ../../plugins/funind -I ../../plugins/firstorder \
+              -I ../../plugins/field -I ../../plugins/subtac -I ../../plugins/rtauto \
+              -I ../../plugins/recdef
 
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index de68ce1e5..46ba24da7 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -744,28 +744,28 @@ Conflicts exists between integers and constrs.
 \nlsep \TERM{simplif}
 \nlsep \TERM{intuition}~\OPT{\NTL{tactic}{0}}
 \nlsep \TERM{linearintuition}~\OPT{\NT{num}}
-%% contrib/cc
+%% plugins/cc
 \nlsep \TERM{cc}
-%% contrib/field
+%% plugins/field
 \nlsep \TERM{field}~\STAR{\tacconstr}
-%% contrib/firstorder
+%% plugins/firstorder
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{with}~\PLUS{\NT{reference}}
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{using}~\PLUS{\NT{ident}}
 %%\nlsep \TERM{gtauto}
 \nlsep \TERM{gintuition}~\OPT{\NTL{tactic}{0}}
-%% contrib/fourier
+%% plugins/fourier
 \nlsep \TERM{fourierZ}
-%% contrib/funind
+%% plugins/funind
 \nlsep \TERM{functional}~\TERM{induction}~\tacconstr~\PLUS{\tacconstr}
-%% contrib/jprover
+%% plugins/jprover
 \nlsep \TERM{jp}~\OPT{\NT{num}}
-%% contrib/omega
+%% plugins/omega
 \nlsep \TERM{omega}
-%% contrib/ring
+%% plugins/ring
 \nlsep \TERM{quote}~\NT{ident}~\OPTGR{\KWD{[}~\PLUS{\NT{ident}}~\KWD{]}}
 \nlsep \TERM{ring}~\STAR{\tacconstr}
-%% contrib/romega
+%% plugins/romega
 \nlsep \TERM{romega}
 \SEPDEF
 \DEFNT{orient}
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
diff --git a/contrib/cc/README b/plugins/cc/README
index 073b140ea..073b140ea 100644
--- a/contrib/cc/README
+++ b/plugins/cc/README
diff --git a/contrib/cc/cc_plugin.mllib b/plugins/cc/cc_plugin.mllib
index 27e903fd3..27e903fd3 100644
--- a/contrib/cc/cc_plugin.mllib
+++ b/plugins/cc/cc_plugin.mllib
diff --git a/contrib/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 2d7dd9d6c..2d7dd9d6c 100644
--- a/contrib/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
diff --git a/contrib/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 3bd52b6e1..3bd52b6e1 100644
--- a/contrib/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
diff --git a/contrib/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 1e57aa6cb..1e57aa6cb 100644
--- a/contrib/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
diff --git a/contrib/cc/ccproof.mli b/plugins/cc/ccproof.mli
index 7fd28390f..7fd28390f 100644
--- a/contrib/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
diff --git a/contrib/cc/cctac.ml b/plugins/cc/cctac.ml
index 515d4aa93..515d4aa93 100644
--- a/contrib/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
diff --git a/contrib/cc/cctac.mli b/plugins/cc/cctac.mli
index 7cdd46ab4..7cdd46ab4 100644
--- a/contrib/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
diff --git a/contrib/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index f23ed49b6..f23ed49b6 100644
--- a/contrib/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
diff --git a/contrib/dp/Dp.v b/plugins/dp/Dp.v
index 47d67725f..47d67725f 100644
--- a/contrib/dp/Dp.v
+++ b/plugins/dp/Dp.v
diff --git a/contrib/dp/TODO b/plugins/dp/TODO
index 44349e214..44349e214 100644
--- a/contrib/dp/TODO
+++ b/plugins/dp/TODO
diff --git a/contrib/dp/dp.ml b/plugins/dp/dp.ml
index 79ffaf3f9..79ffaf3f9 100644
--- a/contrib/dp/dp.ml
+++ b/plugins/dp/dp.ml
diff --git a/contrib/dp/dp.mli b/plugins/dp/dp.mli
index 6dbc05e17..6dbc05e17 100644
--- a/contrib/dp/dp.mli
+++ b/plugins/dp/dp.mli
diff --git a/contrib/dp/dp_gappa.ml b/plugins/dp/dp_gappa.ml
index 9c035aa85..9c035aa85 100644
--- a/contrib/dp/dp_gappa.ml
+++ b/plugins/dp/dp_gappa.ml
diff --git a/contrib/dp/dp_plugin.mllib b/plugins/dp/dp_plugin.mllib
index 361d6f832..361d6f832 100644
--- a/contrib/dp/dp_plugin.mllib
+++ b/plugins/dp/dp_plugin.mllib
diff --git a/contrib/dp/dp_why.ml b/plugins/dp/dp_why.ml
index e24049ad6..e24049ad6 100644
--- a/contrib/dp/dp_why.ml
+++ b/plugins/dp/dp_why.ml
diff --git a/contrib/dp/dp_why.mli b/plugins/dp/dp_why.mli
index b38a3d376..b38a3d376 100644
--- a/contrib/dp/dp_why.mli
+++ b/plugins/dp/dp_why.mli
diff --git a/contrib/dp/dp_zenon.mli b/plugins/dp/dp_zenon.mli
index 0a727d1f1..0a727d1f1 100644
--- a/contrib/dp/dp_zenon.mli
+++ b/plugins/dp/dp_zenon.mli
diff --git a/contrib/dp/dp_zenon.mll b/plugins/dp/dp_zenon.mll
index e15e280db..e15e280db 100644
--- a/contrib/dp/dp_zenon.mll
+++ b/plugins/dp/dp_zenon.mll
diff --git a/contrib/dp/fol.mli b/plugins/dp/fol.mli
index b94bd3e35..b94bd3e35 100644
--- a/contrib/dp/fol.mli
+++ b/plugins/dp/fol.mli
diff --git a/contrib/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4
index 95135694d..95135694d 100644
--- a/contrib/dp/g_dp.ml4
+++ b/plugins/dp/g_dp.ml4
diff --git a/contrib/dp/test2.v b/plugins/dp/test2.v
index 3e4c0f6dd..3e4c0f6dd 100644
--- a/contrib/dp/test2.v
+++ b/plugins/dp/test2.v
diff --git a/contrib/dp/test_gappa.v b/plugins/dp/test_gappa.v
index eb65a59d6..eb65a59d6 100644
--- a/contrib/dp/test_gappa.v
+++ b/plugins/dp/test_gappa.v
diff --git a/contrib/dp/tests.v b/plugins/dp/tests.v
index a6d4f2e13..fa6a13ef0 100644
--- a/contrib/dp/tests.v
+++ b/plugins/dp/tests.v
@@ -160,7 +160,7 @@ simplify.
 Qed.
 
 
-(* Inductive types definitions - call to incontrib/dp/jection function *)
+(* Inductive types definitions - call to dp/injection function *)
 
 Inductive even : Z -> Prop :=
 | even_0 : even 0
diff --git a/contrib/dp/zenon.v b/plugins/dp/zenon.v
index 502465c6b..502465c6b 100644
--- a/contrib/dp/zenon.v
+++ b/plugins/dp/zenon.v
diff --git a/contrib/extraction/CHANGES b/plugins/extraction/CHANGES
index 94531c47e..fbcd01a15 100644
--- a/contrib/extraction/CHANGES
+++ b/plugins/extraction/CHANGES
@@ -79,7 +79,7 @@ but also a few steps toward a more user-friendly extraction:
   were one would have been enough. 
   
   - Examples of code needing those Obj.magic: 
-     * contrib/extraction/test_extraction.v in the Coq source
+     * plugins/extraction/test_extraction.v in the Coq source
      * in the users' contributions: 
 	Lannion
 	Lyon/CIRCUITS
diff --git a/contrib/extraction/README b/plugins/extraction/README
index 64c871fd3..64c871fd3 100644
--- a/contrib/extraction/README
+++ b/plugins/extraction/README
diff --git a/contrib/extraction/common.ml b/plugins/extraction/common.ml
index 11c3b3b5b..11c3b3b5b 100644
--- a/contrib/extraction/common.ml
+++ b/plugins/extraction/common.ml
diff --git a/contrib/extraction/common.mli b/plugins/extraction/common.mli
index c401bd059..c401bd059 100644
--- a/contrib/extraction/common.mli
+++ b/plugins/extraction/common.mli
diff --git a/contrib/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 39e277081..39e277081 100644
--- a/contrib/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
diff --git a/contrib/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index dcb4601e5..dcb4601e5 100644
--- a/contrib/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
diff --git a/contrib/extraction/extraction.ml b/plugins/extraction/extraction.ml
index ffaefd5e3..ffaefd5e3 100644
--- a/contrib/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
diff --git a/contrib/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 2c534ea7b..2c534ea7b 100644
--- a/contrib/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
diff --git a/contrib/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mllib
index bb87b9e32..bb87b9e32 100644
--- a/contrib/extraction/extraction_plugin.mllib
+++ b/plugins/extraction/extraction_plugin.mllib
diff --git a/contrib/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 2b561616b..2b561616b 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
diff --git a/contrib/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 6403e7bbe..6403e7bbe 100644
--- a/contrib/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
diff --git a/contrib/extraction/haskell.mli b/plugins/extraction/haskell.mli
index 1b5dbc711..1b5dbc711 100644
--- a/contrib/extraction/haskell.mli
+++ b/plugins/extraction/haskell.mli
diff --git a/contrib/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 12ca9ad75..12ca9ad75 100644
--- a/contrib/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
diff --git a/contrib/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 213df31e6..213df31e6 100644
--- a/contrib/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
diff --git a/contrib/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 4b6b47ab9..4b6b47ab9 100644
--- a/contrib/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
diff --git a/contrib/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 0394ea4b7..0394ea4b7 100644
--- a/contrib/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
diff --git a/contrib/extraction/modutil.mli b/plugins/extraction/modutil.mli
index 8e04a368e..8e04a368e 100644
--- a/contrib/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
diff --git a/contrib/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 93fc2c2dc..93fc2c2dc 100644
--- a/contrib/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
diff --git a/contrib/extraction/ocaml.mli b/plugins/extraction/ocaml.mli
index 4a1c1778f..4a1c1778f 100644
--- a/contrib/extraction/ocaml.mli
+++ b/plugins/extraction/ocaml.mli
diff --git a/contrib/extraction/scheme.ml b/plugins/extraction/scheme.ml
index eaa47f5f9..eaa47f5f9 100644
--- a/contrib/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
diff --git a/contrib/extraction/scheme.mli b/plugins/extraction/scheme.mli
index b0fa395c6..b0fa395c6 100644
--- a/contrib/extraction/scheme.mli
+++ b/plugins/extraction/scheme.mli
diff --git a/contrib/extraction/table.ml b/plugins/extraction/table.ml
index f1e8f42fe..f1e8f42fe 100644
--- a/contrib/extraction/table.ml
+++ b/plugins/extraction/table.ml
diff --git a/contrib/extraction/table.mli b/plugins/extraction/table.mli
index 6e3f2ec56..6e3f2ec56 100644
--- a/contrib/extraction/table.mli
+++ b/plugins/extraction/table.mli
diff --git a/contrib/field/LegacyField.v b/plugins/field/LegacyField.v
index efa53b4e9..efa53b4e9 100644
--- a/contrib/field/LegacyField.v
+++ b/plugins/field/LegacyField.v
diff --git a/contrib/field/LegacyField_Compl.v b/plugins/field/LegacyField_Compl.v
index 746e7c997..746e7c997 100644
--- a/contrib/field/LegacyField_Compl.v
+++ b/plugins/field/LegacyField_Compl.v
diff --git a/contrib/field/LegacyField_Tactic.v b/plugins/field/LegacyField_Tactic.v
index 63d9bdda6..63d9bdda6 100644
--- a/contrib/field/LegacyField_Tactic.v
+++ b/plugins/field/LegacyField_Tactic.v
diff --git a/contrib/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v
index 131ba84b8..131ba84b8 100644
--- a/contrib/field/LegacyField_Theory.v
+++ b/plugins/field/LegacyField_Theory.v
diff --git a/contrib/field/field.ml4 b/plugins/field/field.ml4
index 93de6118b..93de6118b 100644
--- a/contrib/field/field.ml4
+++ b/plugins/field/field.ml4
diff --git a/contrib/field/field_plugin.mllib b/plugins/field/field_plugin.mllib
index 63492a64f..63492a64f 100644
--- a/contrib/field/field_plugin.mllib
+++ b/plugins/field/field_plugin.mllib
diff --git a/contrib/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 0be3a4b39..0be3a4b39 100644
--- a/contrib/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
diff --git a/contrib/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 9e9d1e122..9e9d1e122 100644
--- a/contrib/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
diff --git a/contrib/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index d7c5b66ae..d7c5b66ae 100644
--- a/contrib/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
diff --git a/contrib/firstorder/ground.ml b/plugins/firstorder/ground.ml
index a8d5fc2ef..a8d5fc2ef 100644
--- a/contrib/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
diff --git a/contrib/firstorder/ground.mli b/plugins/firstorder/ground.mli
index 3c0e903fd..3c0e903fd 100644
--- a/contrib/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
diff --git a/contrib/firstorder/ground_plugin.mllib b/plugins/firstorder/ground_plugin.mllib
index 863ccb50e..863ccb50e 100644
--- a/contrib/firstorder/ground_plugin.mllib
+++ b/plugins/firstorder/ground_plugin.mllib
diff --git a/contrib/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 3e087cd8b..3e087cd8b 100644
--- a/contrib/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
diff --git a/contrib/firstorder/instances.mli b/plugins/firstorder/instances.mli
index aed2ec83d..aed2ec83d 100644
--- a/contrib/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
diff --git a/contrib/firstorder/rules.ml b/plugins/firstorder/rules.ml
index fc31ee6fc..fc31ee6fc 100644
--- a/contrib/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
diff --git a/contrib/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 1c2c93a49..1c2c93a49 100644
--- a/contrib/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
diff --git a/contrib/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index fd5972fb7..fd5972fb7 100644
--- a/contrib/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
diff --git a/contrib/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 51db9de16..51db9de16 100644
--- a/contrib/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
diff --git a/contrib/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 782129e5c..782129e5c 100644
--- a/contrib/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
diff --git a/contrib/firstorder/unify.mli b/plugins/firstorder/unify.mli
index d6cb3a082..d6cb3a082 100644
--- a/contrib/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
diff --git a/contrib/fourier/Fourier.v b/plugins/fourier/Fourier.v
index 07b2973a4..07b2973a4 100644
--- a/contrib/fourier/Fourier.v
+++ b/plugins/fourier/Fourier.v
diff --git a/contrib/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v
index c592af09a..c592af09a 100644
--- a/contrib/fourier/Fourier_util.v
+++ b/plugins/fourier/Fourier_util.v
diff --git a/contrib/fourier/fourier.ml b/plugins/fourier/fourier.ml
index dd54aea29..dd54aea29 100644
--- a/contrib/fourier/fourier.ml
+++ b/plugins/fourier/fourier.ml
diff --git a/contrib/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 908267700..908267700 100644
--- a/contrib/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
diff --git a/contrib/fourier/fourier_plugin.mllib b/plugins/fourier/fourier_plugin.mllib
index b6262f8ae..b6262f8ae 100644
--- a/contrib/fourier/fourier_plugin.mllib
+++ b/plugins/fourier/fourier_plugin.mllib
diff --git a/contrib/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index b952851fa..b952851fa 100644
--- a/contrib/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.ml4
diff --git a/contrib/funind/Recdef.v b/plugins/funind/Recdef.v
index 2d206220e..2d206220e 100644
--- a/contrib/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
diff --git a/contrib/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index adfb9ce2f..adfb9ce2f 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
diff --git a/contrib/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 62eb528e0..62eb528e0 100644
--- a/contrib/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
diff --git a/contrib/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 49d1a179b..49d1a179b 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
diff --git a/contrib/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index cf28c6e6c..cf28c6e6c 100644
--- a/contrib/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
diff --git a/contrib/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 28fec2e98..28fec2e98 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
diff --git a/contrib/funind/indfun.ml b/plugins/funind/indfun.ml
index 348a17b11..348a17b11 100644
--- a/contrib/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
diff --git a/contrib/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 69cc0607b..69cc0607b 100644
--- a/contrib/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
diff --git a/contrib/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index e9aa692b6..e9aa692b6 100644
--- a/contrib/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
diff --git a/contrib/funind/invfun.ml b/plugins/funind/invfun.ml
index 5f8587408..5f8587408 100644
--- a/contrib/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
diff --git a/contrib/funind/merge.ml b/plugins/funind/merge.ml
index 9bbd165df..092830025 100644
--- a/contrib/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -1028,7 +1028,7 @@ let relprinctype_to_funprinctype relprinctype nfuns =
  *)
 (* 
 *** Local Variables: ***
-*** compile-command: "make -C ../.. contrib/funind/merge.cmo" ***
+*** compile-command: "make -C ../.. plugins/funind/merge.cmo" ***
 *** indent-tabs-mode: nil ***
 *** End: ***
 *)
diff --git a/contrib/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 7e9ba3f8e..7e9ba3f8e 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
diff --git a/contrib/funind/rawterm_to_relation.mli b/plugins/funind/rawterm_to_relation.mli
index 0075fb0a0..0075fb0a0 100644
--- a/contrib/funind/rawterm_to_relation.mli
+++ b/plugins/funind/rawterm_to_relation.mli
diff --git a/contrib/funind/rawtermops.ml b/plugins/funind/rawtermops.ml
index 92396af59..92396af59 100644
--- a/contrib/funind/rawtermops.ml
+++ b/plugins/funind/rawtermops.ml
diff --git a/contrib/funind/rawtermops.mli b/plugins/funind/rawtermops.mli
index 358c6ba6c..358c6ba6c 100644
--- a/contrib/funind/rawtermops.mli
+++ b/plugins/funind/rawtermops.mli
diff --git a/contrib/funind/recdef.ml b/plugins/funind/recdef.ml
index a96ec6a43..a96ec6a43 100644
--- a/contrib/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
diff --git a/contrib/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mllib
index c30ee212f..c30ee212f 100644
--- a/contrib/funind/recdef_plugin.mllib
+++ b/plugins/funind/recdef_plugin.mllib
diff --git a/contrib/groebner/GroebnerR.v b/plugins/groebner/GroebnerR.v
index 71e244126..71e244126 100644
--- a/contrib/groebner/GroebnerR.v
+++ b/plugins/groebner/GroebnerR.v
diff --git a/contrib/groebner/GroebnerZ.v b/plugins/groebner/GroebnerZ.v
index da79a36f7..da79a36f7 100644
--- a/contrib/groebner/GroebnerZ.v
+++ b/plugins/groebner/GroebnerZ.v
diff --git a/contrib/groebner/groebner.ml4 b/plugins/groebner/groebner.ml4
index 00cd8ae5d..00cd8ae5d 100644
--- a/contrib/groebner/groebner.ml4
+++ b/plugins/groebner/groebner.ml4
diff --git a/contrib/groebner/groebner_plugin.mllib b/plugins/groebner/groebner_plugin.mllib
index 1da12fcf2..1da12fcf2 100644
--- a/contrib/groebner/groebner_plugin.mllib
+++ b/plugins/groebner/groebner_plugin.mllib
diff --git a/contrib/groebner/ideal.ml b/plugins/groebner/ideal.ml
index a87a9972b..a87a9972b 100644
--- a/contrib/groebner/ideal.ml
+++ b/plugins/groebner/ideal.ml
diff --git a/contrib/groebner/ideal.mli b/plugins/groebner/ideal.mli
index 48b81102e..48b81102e 100644
--- a/contrib/groebner/ideal.mli
+++ b/plugins/groebner/ideal.mli
diff --git a/contrib/groebner/polynom.ml b/plugins/groebner/polynom.ml
index 5c859f755..5c859f755 100644
--- a/contrib/groebner/polynom.ml
+++ b/plugins/groebner/polynom.ml
diff --git a/contrib/groebner/polynom.mli b/plugins/groebner/polynom.mli
index 99c1701b8..99c1701b8 100644
--- a/contrib/groebner/polynom.mli
+++ b/plugins/groebner/polynom.mli
diff --git a/contrib/groebner/utile.ml b/plugins/groebner/utile.ml
index 52a69dc10..52a69dc10 100644
--- a/contrib/groebner/utile.ml
+++ b/plugins/groebner/utile.ml
diff --git a/contrib/groebner/utile.mli b/plugins/groebner/utile.mli
index 209258dd6..209258dd6 100644
--- a/contrib/groebner/utile.mli
+++ b/plugins/groebner/utile.mli
diff --git a/contrib/interface/COPYRIGHT b/plugins/interface/COPYRIGHT
index 23aeb6bb2..824838309 100644
--- a/contrib/interface/COPYRIGHT
+++ b/plugins/interface/COPYRIGHT
@@ -7,7 +7,7 @@
 (*                                                                           *)
 (*****************************************************************************)
 
-The current directory contrib/interface implements Coq support for the
+The current directory plugins/interface implements Coq support for the
 Pcoq Graphical Interface of Coq. It has been developed by Yves Bertot
 with contributions from Loïc Pottier and Laurence Rideau.
 
diff --git a/contrib/interface/CoqInterface.v b/plugins/interface/CoqInterface.v
index e86fb2fce..e86fb2fce 100644
--- a/contrib/interface/CoqInterface.v
+++ b/plugins/interface/CoqInterface.v
diff --git a/contrib/interface/CoqParser.v b/plugins/interface/CoqParser.v
index db4aa06dc..db4aa06dc 100644
--- a/contrib/interface/CoqParser.v
+++ b/plugins/interface/CoqParser.v
diff --git a/contrib/interface/ascent.mli b/plugins/interface/ascent.mli
index f0b68fb7c..f0b68fb7c 100644
--- a/contrib/interface/ascent.mli
+++ b/plugins/interface/ascent.mli
diff --git a/contrib/interface/blast.ml b/plugins/interface/blast.ml
index 57b4d1af8..57b4d1af8 100644
--- a/contrib/interface/blast.ml
+++ b/plugins/interface/blast.ml
diff --git a/contrib/interface/blast.mli b/plugins/interface/blast.mli
index f67019439..f67019439 100644
--- a/contrib/interface/blast.mli
+++ b/plugins/interface/blast.mli
diff --git a/contrib/interface/centaur.ml4 b/plugins/interface/centaur.ml4
index f8c088779..f8c088779 100644
--- a/contrib/interface/centaur.ml4
+++ b/plugins/interface/centaur.ml4
diff --git a/contrib/interface/coqinterface_plugin.mllib b/plugins/interface/coqinterface_plugin.mllib
index e4b575b13..e4b575b13 100644
--- a/contrib/interface/coqinterface_plugin.mllib
+++ b/plugins/interface/coqinterface_plugin.mllib
diff --git a/contrib/interface/coqparser.ml b/plugins/interface/coqparser.ml
index 5de6060f0..a63e18d27 100644
--- a/contrib/interface/coqparser.ml
+++ b/plugins/interface/coqparser.ml
@@ -378,7 +378,7 @@ Libobject.relax true;
      begin
        add_rec_path (Filename.concat coqdir "theories")
 	 (Names.make_dirpath [Nameops.coq_root]);
-       add_rec_path (Filename.concat coqdir "contrib")
+       add_rec_path (Filename.concat coqdir "plugins")
 	 (Names.make_dirpath [Nameops.coq_root])
      end;
 (let vernacrc =
@@ -388,7 +388,7 @@ Libobject.relax true;
        Not_found -> 
 	 List.fold_left 
 	   (fun s1 s2 -> (Filename.concat s1 s2))
-	   coqdir [ "contrib"; "interface"; "vernacrc"] in
+	   coqdir [ "plugins"; "interface"; "vernacrc"] in
    try
      (Gramext.warning_verbose := false;
       coqparser_loop (open_in vernacrc))
diff --git a/contrib/interface/coqparser_plugin.mllib b/plugins/interface/coqparser_plugin.mllib
index 65ec57715..65ec57715 100644
--- a/contrib/interface/coqparser_plugin.mllib
+++ b/plugins/interface/coqparser_plugin.mllib
diff --git a/contrib/interface/dad.ml b/plugins/interface/dad.ml
index c2ab2dc8d..c2ab2dc8d 100644
--- a/contrib/interface/dad.ml
+++ b/plugins/interface/dad.ml
diff --git a/contrib/interface/dad.mli b/plugins/interface/dad.mli
index f556c1926..f556c1926 100644
--- a/contrib/interface/dad.mli
+++ b/plugins/interface/dad.mli
diff --git a/contrib/interface/debug_tac.ml4 b/plugins/interface/debug_tac.ml4
index aad3a765d..aad3a765d 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/plugins/interface/debug_tac.ml4
diff --git a/contrib/interface/debug_tac.mli b/plugins/interface/debug_tac.mli
index da4bbaa09..da4bbaa09 100644
--- a/contrib/interface/debug_tac.mli
+++ b/plugins/interface/debug_tac.mli
diff --git a/contrib/interface/depends.ml b/plugins/interface/depends.ml
index e59de34a4..e59de34a4 100644
--- a/contrib/interface/depends.ml
+++ b/plugins/interface/depends.ml
diff --git a/contrib/interface/history.ml b/plugins/interface/history.ml
index f73c20849..f73c20849 100644
--- a/contrib/interface/history.ml
+++ b/plugins/interface/history.ml
diff --git a/contrib/interface/history.mli b/plugins/interface/history.mli
index 053883f0d..053883f0d 100644
--- a/contrib/interface/history.mli
+++ b/plugins/interface/history.mli
diff --git a/contrib/interface/line_parser.ml4 b/plugins/interface/line_parser.ml4
index 0b13a092a..0b13a092a 100755
--- a/contrib/interface/line_parser.ml4
+++ b/plugins/interface/line_parser.ml4
diff --git a/contrib/interface/line_parser.mli b/plugins/interface/line_parser.mli
index b0b043c75..b0b043c75 100644
--- a/contrib/interface/line_parser.mli
+++ b/plugins/interface/line_parser.mli
diff --git a/contrib/interface/name_to_ast.ml b/plugins/interface/name_to_ast.ml
index 668a581e1..668a581e1 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/plugins/interface/name_to_ast.ml
diff --git a/contrib/interface/name_to_ast.mli b/plugins/interface/name_to_ast.mli
index f9e83b5e1..f9e83b5e1 100644
--- a/contrib/interface/name_to_ast.mli
+++ b/plugins/interface/name_to_ast.mli
diff --git a/contrib/interface/paths.ml b/plugins/interface/paths.ml
index a157ca925..a157ca925 100644
--- a/contrib/interface/paths.ml
+++ b/plugins/interface/paths.ml
diff --git a/contrib/interface/paths.mli b/plugins/interface/paths.mli
index 266207238..266207238 100644
--- a/contrib/interface/paths.mli
+++ b/plugins/interface/paths.mli
diff --git a/contrib/interface/pbp.ml b/plugins/interface/pbp.ml
index 01747aa58..01747aa58 100644
--- a/contrib/interface/pbp.ml
+++ b/plugins/interface/pbp.ml
diff --git a/contrib/interface/pbp.mli b/plugins/interface/pbp.mli
index 9daba1844..9daba1844 100644
--- a/contrib/interface/pbp.mli
+++ b/plugins/interface/pbp.mli
diff --git a/contrib/interface/showproof.ml b/plugins/interface/showproof.ml
index 2ab62763d..2ab62763d 100644
--- a/contrib/interface/showproof.ml
+++ b/plugins/interface/showproof.ml
diff --git a/contrib/interface/showproof.mli b/plugins/interface/showproof.mli
index 9b6787b7c..9b6787b7c 100755
--- a/contrib/interface/showproof.mli
+++ b/plugins/interface/showproof.mli
diff --git a/contrib/interface/showproof_ct.ml b/plugins/interface/showproof_ct.ml
index dd7f455d7..dd7f455d7 100644
--- a/contrib/interface/showproof_ct.ml
+++ b/plugins/interface/showproof_ct.ml
diff --git a/contrib/interface/translate.ml b/plugins/interface/translate.ml
index 559860b2f..559860b2f 100644
--- a/contrib/interface/translate.ml
+++ b/plugins/interface/translate.ml
diff --git a/contrib/interface/translate.mli b/plugins/interface/translate.mli
index 34841fc4b..34841fc4b 100644
--- a/contrib/interface/translate.mli
+++ b/plugins/interface/translate.mli
diff --git a/contrib/interface/vernacrc b/plugins/interface/vernacrc
index 14f7e8c98..14f7e8c98 100644
--- a/contrib/interface/vernacrc
+++ b/plugins/interface/vernacrc
diff --git a/contrib/interface/vtp.ml b/plugins/interface/vtp.ml
index 1714440df..1714440df 100644
--- a/contrib/interface/vtp.ml
+++ b/plugins/interface/vtp.ml
diff --git a/contrib/interface/vtp.mli b/plugins/interface/vtp.mli
index d7bd8db53..d7bd8db53 100644
--- a/contrib/interface/vtp.mli
+++ b/plugins/interface/vtp.mli
diff --git a/contrib/interface/xlate.ml b/plugins/interface/xlate.ml
index 64a9b5c8c..64a9b5c8c 100644
--- a/contrib/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
diff --git a/contrib/interface/xlate.mli b/plugins/interface/xlate.mli
index 2e2b95fe7..2e2b95fe7 100644
--- a/contrib/interface/xlate.mli
+++ b/plugins/interface/xlate.mli
diff --git a/contrib/micromega/CheckerMaker.v b/plugins/micromega/CheckerMaker.v
index 93b4d213f..93b4d213f 100644
--- a/contrib/micromega/CheckerMaker.v
+++ b/plugins/micromega/CheckerMaker.v
diff --git a/contrib/micromega/Env.v b/plugins/micromega/Env.v
index 40db9e464..631417e0e 100644
--- a/contrib/micromega/Env.v
+++ b/plugins/micromega/Env.v
@@ -17,7 +17,7 @@ Require Import Coq.Arith.Max.
 Require Import List.
 Set Implicit Arguments.
 
-(* I have addded a Leaf constructor to the varmap data structure (/contrib/ring/Quote.v) 
+(* I have addded a Leaf constructor to the varmap data structure (/plugins/ring/Quote.v) 
    -- this is harmless and spares a lot of Empty.
    This means smaller proof-terms. 
    BTW, by dropping the  polymorphism, I get small (yet noticeable) speed-up.
diff --git a/contrib/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 04e68272e..04e68272e 100644
--- a/contrib/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
diff --git a/contrib/micromega/LICENSE.sos b/plugins/micromega/LICENSE.sos
index 5aadfa2a6..5aadfa2a6 100644
--- a/contrib/micromega/LICENSE.sos
+++ b/plugins/micromega/LICENSE.sos
diff --git a/contrib/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index a5ac92db8..a5ac92db8 100644
--- a/contrib/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
diff --git a/contrib/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v
index 149b77316..149b77316 100644
--- a/contrib/micromega/OrderedRing.v
+++ b/plugins/micromega/OrderedRing.v
diff --git a/contrib/micromega/Psatz.v b/plugins/micromega/Psatz.v
index a3be56207..a3be56207 100644
--- a/contrib/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
diff --git a/contrib/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index f02209459..f02209459 100644
--- a/contrib/micromega/QMicromega.v
+++ b/plugins/micromega/QMicromega.v
diff --git a/contrib/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 70786a057..70786a057 100644
--- a/contrib/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
diff --git a/contrib/micromega/Refl.v b/plugins/micromega/Refl.v
index 801d8b212..801d8b212 100644
--- a/contrib/micromega/Refl.v
+++ b/plugins/micromega/Refl.v
diff --git a/contrib/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 6885b82cd..6885b82cd 100644
--- a/contrib/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
diff --git a/contrib/micromega/Tauto.v b/plugins/micromega/Tauto.v
index ef48efa6d..ef48efa6d 100644
--- a/contrib/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
diff --git a/contrib/micromega/VarMap.v b/plugins/micromega/VarMap.v
index 240c0fb7c..ed204d92b 100644
--- a/contrib/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -17,7 +17,7 @@ Require Import Coq.Arith.Max.
 Require Import List.
 Set Implicit Arguments.
 
-(* I have addded a Leaf constructor to the varmap data structure (/contrib/ring/Quote.v) 
+(* I have addded a Leaf constructor to the varmap data structure (/plugins/ring/Quote.v) 
    -- this is harmless and spares a lot of Empty.
    This means smaller proof-terms. 
    BTW, by dropping the  polymorphism, I get small (yet noticeable) speed-up.
@@ -43,7 +43,7 @@ Section MakeVarMap.
                       end
     end.
 
- (* an off_map (a map with offset) offers the same functionalites  as /contrib/setoid_ring/BinList.v - it is used in EnvRing.v *)
+ (* an off_map (a map with offset) offers the same functionalites  as /plugins/setoid_ring/BinList.v - it is used in EnvRing.v *)
 (*
   Definition off_map  :=  (option positive *t )%type.
 
diff --git a/contrib/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index ced67e39d..ced67e39d 100644
--- a/contrib/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
diff --git a/contrib/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 1da3228a9..1da3228a9 100644
--- a/contrib/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
diff --git a/contrib/micromega/certificate.ml b/plugins/micromega/certificate.ml
index a297c1633..a297c1633 100644
--- a/contrib/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
diff --git a/contrib/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index e9a8a0e3b..3e88af9f0 100644
--- a/contrib/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1295,7 +1295,7 @@ let call_csdpcert provername poly =
   close_out ch_to;
   let cmdname =
     List.fold_left Filename.concat (Envars.coqlib ())
-      ["contrib"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in
+      ["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in
   let c = Sys.command (cmdname ^" "^ tmp_to ^" "^ tmp_from) in
   (try Sys.remove tmp_to with _ -> ());
   if c <> 0 then Util.error ("Failed to call csdp certificate generator");
diff --git a/contrib/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index e451a38fd..e451a38fd 100644
--- a/contrib/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
diff --git a/contrib/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 23ae3bd0e..23ae3bd0e 100644
--- a/contrib/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
diff --git a/contrib/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index c2eb572c9..c2eb572c9 100644
--- a/contrib/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
diff --git a/contrib/micromega/micromega.ml b/plugins/micromega/micromega.ml
index e151e4e1d..e151e4e1d 100644
--- a/contrib/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
diff --git a/contrib/micromega/micromega.mli b/plugins/micromega/micromega.mli
index f94f091e8..f94f091e8 100644
--- a/contrib/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
diff --git a/contrib/micromega/micromega_plugin.mllib b/plugins/micromega/micromega_plugin.mllib
index 41753542f..41753542f 100644
--- a/contrib/micromega/micromega_plugin.mllib
+++ b/plugins/micromega/micromega_plugin.mllib
diff --git a/contrib/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 03e3999fd..03e3999fd 100644
--- a/contrib/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
diff --git a/contrib/micromega/sos.ml b/plugins/micromega/sos.ml
index e3d72ed9a..e3d72ed9a 100644
--- a/contrib/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
diff --git a/contrib/micromega/sos.mli b/plugins/micromega/sos.mli
index 31c9518c8..31c9518c8 100644
--- a/contrib/micromega/sos.mli
+++ b/plugins/micromega/sos.mli
diff --git a/contrib/omega/Omega.v b/plugins/omega/Omega.v
index 30b945718..30b945718 100644
--- a/contrib/omega/Omega.v
+++ b/plugins/omega/Omega.v
diff --git a/contrib/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v
index fe8fcc924..fe8fcc924 100644
--- a/contrib/omega/OmegaLemmas.v
+++ b/plugins/omega/OmegaLemmas.v
diff --git a/contrib/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v
index 21535f0d3..21535f0d3 100644
--- a/contrib/omega/OmegaPlugin.v
+++ b/plugins/omega/OmegaPlugin.v
diff --git a/contrib/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 47e22a97f..47e22a97f 100644
--- a/contrib/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
diff --git a/contrib/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 535459885..535459885 100644
--- a/contrib/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
diff --git a/contrib/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index a69f8ef74..a69f8ef74 100644
--- a/contrib/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
diff --git a/contrib/omega/omega.ml b/plugins/omega/omega.ml
index fd774c16d..fd774c16d 100644
--- a/contrib/omega/omega.ml
+++ b/plugins/omega/omega.ml
diff --git a/contrib/omega/omega_plugin.mllib b/plugins/omega/omega_plugin.mllib
index 020901376..020901376 100644
--- a/contrib/omega/omega_plugin.mllib
+++ b/plugins/omega/omega_plugin.mllib
diff --git a/contrib/quote/Quote.v b/plugins/quote/Quote.v
index f21a678e1..f21a678e1 100644
--- a/contrib/quote/Quote.v
+++ b/plugins/quote/Quote.v
diff --git a/contrib/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 808cbbf27..808cbbf27 100644
--- a/contrib/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
diff --git a/contrib/quote/quote.ml b/plugins/quote/quote.ml
index 9141dc2f5..9141dc2f5 100644
--- a/contrib/quote/quote.ml
+++ b/plugins/quote/quote.ml
diff --git a/contrib/quote/quote_plugin.mllib b/plugins/quote/quote_plugin.mllib
index 21810acdf..21810acdf 100644
--- a/contrib/quote/quote_plugin.mllib
+++ b/plugins/quote/quote_plugin.mllib
diff --git a/contrib/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v
index 959d66c74..959d66c74 100644
--- a/contrib/ring/LegacyArithRing.v
+++ b/plugins/ring/LegacyArithRing.v
diff --git a/contrib/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v
index ee9fb3761..ee9fb3761 100644
--- a/contrib/ring/LegacyNArithRing.v
+++ b/plugins/ring/LegacyNArithRing.v
diff --git a/contrib/ring/LegacyRing.v b/plugins/ring/LegacyRing.v
index 4ae85baf3..4ae85baf3 100644
--- a/contrib/ring/LegacyRing.v
+++ b/plugins/ring/LegacyRing.v
diff --git a/contrib/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v
index 79f6976bd..79f6976bd 100644
--- a/contrib/ring/LegacyRing_theory.v
+++ b/plugins/ring/LegacyRing_theory.v
diff --git a/contrib/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v
index 68a0dd275..68a0dd275 100644
--- a/contrib/ring/LegacyZArithRing.v
+++ b/plugins/ring/LegacyZArithRing.v
diff --git a/contrib/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v
index 9b85fb85e..9b85fb85e 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/plugins/ring/Ring_abstract.v
diff --git a/contrib/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v
index ad1cc5cf1..ad1cc5cf1 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/plugins/ring/Ring_normalize.v
diff --git a/contrib/ring/Setoid_ring.v b/plugins/ring/Setoid_ring.v
index 93b9bc7cf..93b9bc7cf 100644
--- a/contrib/ring/Setoid_ring.v
+++ b/plugins/ring/Setoid_ring.v
diff --git a/contrib/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v
index ce23d05af..ce23d05af 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/plugins/ring/Setoid_ring_normalize.v
diff --git a/contrib/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v
index f50a2f30a..f50a2f30a 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/plugins/ring/Setoid_ring_theory.v
diff --git a/contrib/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4
index 5ca1bfced..5ca1bfced 100644
--- a/contrib/ring/g_ring.ml4
+++ b/plugins/ring/g_ring.ml4
diff --git a/contrib/ring/ring.ml b/plugins/ring/ring.ml
index adcf51fe8..adcf51fe8 100644
--- a/contrib/ring/ring.ml
+++ b/plugins/ring/ring.ml
diff --git a/contrib/ring/ring_plugin.mllib b/plugins/ring/ring_plugin.mllib
index 183884ca6..183884ca6 100644
--- a/contrib/ring/ring_plugin.mllib
+++ b/plugins/ring/ring_plugin.mllib
diff --git a/contrib/romega/README b/plugins/romega/README
index 86c9e58af..86c9e58af 100644
--- a/contrib/romega/README
+++ b/plugins/romega/README
diff --git a/contrib/romega/ROmega.v b/plugins/romega/ROmega.v
index 3ddb6bed1..3ddb6bed1 100644
--- a/contrib/romega/ROmega.v
+++ b/plugins/romega/ROmega.v
diff --git a/contrib/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 12176d661..12176d661 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
diff --git a/contrib/romega/const_omega.ml b/plugins/romega/const_omega.ml
index bdec6bf45..bdec6bf45 100644
--- a/contrib/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
diff --git a/contrib/romega/const_omega.mli b/plugins/romega/const_omega.mli
index 0f00e9184..0f00e9184 100644
--- a/contrib/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
diff --git a/contrib/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 39b6c2106..39b6c2106 100644
--- a/contrib/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
diff --git a/contrib/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index fc4f7a8f0..fc4f7a8f0 100644
--- a/contrib/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
diff --git a/contrib/romega/romega_plugin.mllib b/plugins/romega/romega_plugin.mllib
index 38d0e9411..38d0e9411 100644
--- a/contrib/romega/romega_plugin.mllib
+++ b/plugins/romega/romega_plugin.mllib
diff --git a/contrib/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index cd0f1afe9..cd0f1afe9 100644
--- a/contrib/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
diff --git a/contrib/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v
index 4b95097e2..4b95097e2 100644
--- a/contrib/rtauto/Rtauto.v
+++ b/plugins/rtauto/Rtauto.v
diff --git a/contrib/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index 4cbe84368..4cbe84368 100644
--- a/contrib/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
diff --git a/contrib/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 9d9d66bb2..9d9d66bb2 100644
--- a/contrib/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
diff --git a/contrib/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli
index a0e86b8d6..a0e86b8d6 100644
--- a/contrib/rtauto/proof_search.mli
+++ b/plugins/rtauto/proof_search.mli
diff --git a/contrib/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 6cde1ddcf..6cde1ddcf 100644
--- a/contrib/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
diff --git a/contrib/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index a6d68a226..a6d68a226 100644
--- a/contrib/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
diff --git a/contrib/rtauto/rtauto_plugin.mllib b/plugins/rtauto/rtauto_plugin.mllib
index 61c5e945b..61c5e945b 100644
--- a/contrib/rtauto/rtauto_plugin.mllib
+++ b/plugins/rtauto/rtauto_plugin.mllib
diff --git a/contrib/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v
index 601cabe00..601cabe00 100644
--- a/contrib/setoid_ring/ArithRing.v
+++ b/plugins/setoid_ring/ArithRing.v
diff --git a/contrib/setoid_ring/BinList.v b/plugins/setoid_ring/BinList.v
index 509020042..509020042 100644
--- a/contrib/setoid_ring/BinList.v
+++ b/plugins/setoid_ring/BinList.v
diff --git a/contrib/setoid_ring/Field.v b/plugins/setoid_ring/Field.v
index a944ba5f0..a944ba5f0 100644
--- a/contrib/setoid_ring/Field.v
+++ b/plugins/setoid_ring/Field.v
diff --git a/contrib/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
index b31ebda55..b31ebda55 100644
--- a/contrib/setoid_ring/Field_tac.v
+++ b/plugins/setoid_ring/Field_tac.v
diff --git a/contrib/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index fd99f786f..fd99f786f 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
diff --git a/contrib/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index e664b3b76..e664b3b76 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
diff --git a/contrib/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v
index 0ba519fde..0ba519fde 100644
--- a/contrib/setoid_ring/NArithRing.v
+++ b/plugins/setoid_ring/NArithRing.v
diff --git a/contrib/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v
index 60641bcf9..60641bcf9 100644
--- a/contrib/setoid_ring/RealField.v
+++ b/plugins/setoid_ring/RealField.v
diff --git a/contrib/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v
index d01b16258..d01b16258 100644
--- a/contrib/setoid_ring/Ring.v
+++ b/plugins/setoid_ring/Ring.v
diff --git a/contrib/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v
index fd9dd8d0d..fd9dd8d0d 100644
--- a/contrib/setoid_ring/Ring_base.v
+++ b/plugins/setoid_ring/Ring_base.v
diff --git a/contrib/setoid_ring/Ring_equiv.v b/plugins/setoid_ring/Ring_equiv.v
index 945f6c684..945f6c684 100644
--- a/contrib/setoid_ring/Ring_equiv.v
+++ b/plugins/setoid_ring/Ring_equiv.v
diff --git a/contrib/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index d88470369..d88470369 100644
--- a/contrib/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
diff --git a/contrib/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index 44e97bda7..44e97bda7 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
diff --git a/contrib/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 531ab3ca5..531ab3ca5 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
diff --git a/contrib/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v
index 942915abf..942915abf 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/plugins/setoid_ring/ZArithRing.v
diff --git a/contrib/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 095e86133..926ac48d1 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -245,29 +245,29 @@ let rec dest_rel t =
 (****************************************************************************)
 (* Library linking *)
 
-let contrib_name = "setoid_ring"
+let plugin_dir = "setoid_ring"
 
-let cdir = ["Coq";contrib_name]
-let contrib_modules =
+let cdir = ["Coq";plugin_dir]
+let plugin_modules =
   List.map (fun d -> cdir@d)
     [["Ring_theory"];["Ring_polynom"]; ["Ring_tac"];["InitialRing"];
      ["Field_tac"]; ["Field_theory"]
     ]
 
 let my_constant c =
-  lazy (Coqlib.gen_constant_in_modules "Ring" contrib_modules c)
+  lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c)
 
 let new_ring_path =
-  make_dirpath (List.map id_of_string ["Ring_tac";contrib_name;"Coq"])
+  make_dirpath (List.map id_of_string ["Ring_tac";plugin_dir;"Coq"])
 let ltac s =
   lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s))
 let znew_ring_path =
-  make_dirpath (List.map id_of_string ["InitialRing";contrib_name;"Coq"])
+  make_dirpath (List.map id_of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
   lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s))
 
 let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);;
-let pol_cst s = mk_cst [contrib_name;"Ring_polynom"] s ;;
+let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
 
 (* Ring theory *)
 
@@ -851,7 +851,7 @@ END
 (***********************************************************************)
 
 let new_field_path =
-  make_dirpath (List.map id_of_string ["Field_tac";contrib_name;"Coq"])
+  make_dirpath (List.map id_of_string ["Field_tac";plugin_dir;"Coq"])
 
 let field_ltac s =
   lazy(make_kn (MPfile new_field_path) (make_dirpath []) (mk_label s))
diff --git a/contrib/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib
index 54b7c8e67..54b7c8e67 100644
--- a/contrib/setoid_ring/newring_plugin.mllib
+++ b/plugins/setoid_ring/newring_plugin.mllib
diff --git a/contrib/subtac/equations.ml4 b/plugins/subtac/equations.ml4
index 5b76c9587..5b76c9587 100644
--- a/contrib/subtac/equations.ml4
+++ b/plugins/subtac/equations.ml4
diff --git a/contrib/subtac/eterm.ml b/plugins/subtac/eterm.ml
index 00a69bba7..00a69bba7 100644
--- a/contrib/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
diff --git a/contrib/subtac/eterm.mli b/plugins/subtac/eterm.mli
index 413823ffe..413823ffe 100644
--- a/contrib/subtac/eterm.mli
+++ b/plugins/subtac/eterm.mli
diff --git a/contrib/subtac/g_eterm.ml4 b/plugins/subtac/g_eterm.ml4
index 095e5fafc..095e5fafc 100644
--- a/contrib/subtac/g_eterm.ml4
+++ b/plugins/subtac/g_eterm.ml4
diff --git a/contrib/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index c1e168da1..c1e168da1 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
diff --git a/contrib/subtac/subtac.ml b/plugins/subtac/subtac.ml
index d10c8f68c..d10c8f68c 100644
--- a/contrib/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
diff --git a/contrib/subtac/subtac.mli b/plugins/subtac/subtac.mli
index b51150aa0..b51150aa0 100644
--- a/contrib/subtac/subtac.mli
+++ b/plugins/subtac/subtac.mli
diff --git a/contrib/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 00ed62ac8..00ed62ac8 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
diff --git a/contrib/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli
index 90989d2d3..90989d2d3 100644
--- a/contrib/subtac/subtac_cases.mli
+++ b/plugins/subtac/subtac_cases.mli
diff --git a/contrib/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 8ef215346..8ef215346 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
diff --git a/contrib/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli
index 917ed8059..917ed8059 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/plugins/subtac/subtac_classes.mli
diff --git a/contrib/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 54114b0b0..54114b0b0 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
diff --git a/contrib/subtac/subtac_coercion.mli b/plugins/subtac/subtac_coercion.mli
index 5678c10e6..5678c10e6 100644
--- a/contrib/subtac/subtac_coercion.mli
+++ b/plugins/subtac/subtac_coercion.mli
diff --git a/contrib/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 674805962..674805962 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
diff --git a/contrib/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
index 3a6a351ba..3a6a351ba 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/plugins/subtac/subtac_command.mli
diff --git a/contrib/subtac/subtac_errors.ml b/plugins/subtac/subtac_errors.ml
index 3bbfe22bc..3bbfe22bc 100644
--- a/contrib/subtac/subtac_errors.ml
+++ b/plugins/subtac/subtac_errors.ml
diff --git a/contrib/subtac/subtac_errors.mli b/plugins/subtac/subtac_errors.mli
index 8d75b9c01..8d75b9c01 100644
--- a/contrib/subtac/subtac_errors.mli
+++ b/plugins/subtac/subtac_errors.mli
diff --git a/contrib/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 8b8bb9ab4..8b8bb9ab4 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
diff --git a/contrib/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 60c0a4139..60c0a4139 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
diff --git a/contrib/subtac/subtac_plugin.mllib b/plugins/subtac/subtac_plugin.mllib
index 81b9ee2ba..81b9ee2ba 100644
--- a/contrib/subtac/subtac_plugin.mllib
+++ b/plugins/subtac/subtac_plugin.mllib
diff --git a/contrib/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index d9df5b34c..d9df5b34c 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
diff --git a/contrib/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli
index 1d8eb2507..1d8eb2507 100644
--- a/contrib/subtac/subtac_pretyping.mli
+++ b/plugins/subtac/subtac_pretyping.mli
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 01fe4ef6f..01fe4ef6f 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
diff --git a/contrib/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index ba30ee190..ba30ee190 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
diff --git a/contrib/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index 964f668f2..964f668f2 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
diff --git a/contrib/subtac/test/ListDep.v b/plugins/subtac/test/ListDep.v
index da612c436..da612c436 100644
--- a/contrib/subtac/test/ListDep.v
+++ b/plugins/subtac/test/ListDep.v
diff --git a/contrib/subtac/test/ListsTest.v b/plugins/subtac/test/ListsTest.v
index 05fc0803f..05fc0803f 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/plugins/subtac/test/ListsTest.v
diff --git a/contrib/subtac/test/Mutind.v b/plugins/subtac/test/Mutind.v
index ac49ca96a..ac49ca96a 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/plugins/subtac/test/Mutind.v
diff --git a/contrib/subtac/test/Test1.v b/plugins/subtac/test/Test1.v
index 14b808549..14b808549 100644
--- a/contrib/subtac/test/Test1.v
+++ b/plugins/subtac/test/Test1.v
diff --git a/contrib/subtac/test/euclid.v b/plugins/subtac/test/euclid.v
index 501aa7981..501aa7981 100644
--- a/contrib/subtac/test/euclid.v
+++ b/plugins/subtac/test/euclid.v
diff --git a/contrib/subtac/test/id.v b/plugins/subtac/test/id.v
index 9ae110881..9ae110881 100644
--- a/contrib/subtac/test/id.v
+++ b/plugins/subtac/test/id.v
diff --git a/contrib/subtac/test/measure.v b/plugins/subtac/test/measure.v
index 4f938f4f8..4f938f4f8 100644
--- a/contrib/subtac/test/measure.v
+++ b/plugins/subtac/test/measure.v
diff --git a/contrib/subtac/test/rec.v b/plugins/subtac/test/rec.v
index aaefd8cc5..aaefd8cc5 100644
--- a/contrib/subtac/test/rec.v
+++ b/plugins/subtac/test/rec.v
diff --git a/contrib/subtac/test/take.v b/plugins/subtac/test/take.v
index 2e17959c3..2e17959c3 100644
--- a/contrib/subtac/test/take.v
+++ b/plugins/subtac/test/take.v
diff --git a/contrib/subtac/test/wf.v b/plugins/subtac/test/wf.v
index 49fec2b80..49fec2b80 100644
--- a/contrib/subtac/test/wf.v
+++ b/plugins/subtac/test/wf.v
diff --git a/contrib/xml/COPYRIGHT b/plugins/xml/COPYRIGHT
index c8d231fd3..c8d231fd3 100644
--- a/contrib/xml/COPYRIGHT
+++ b/plugins/xml/COPYRIGHT
diff --git a/contrib/xml/README b/plugins/xml/README
index a45dd31a5..a45dd31a5 100644
--- a/contrib/xml/README
+++ b/plugins/xml/README
diff --git a/contrib/xml/acic.ml b/plugins/xml/acic.ml
index 032ddbebe..032ddbebe 100644
--- a/contrib/xml/acic.ml
+++ b/plugins/xml/acic.ml
diff --git a/contrib/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
index 64dc8a050..64dc8a050 100644
--- a/contrib/xml/acic2Xml.ml4
+++ b/plugins/xml/acic2Xml.ml4
diff --git a/contrib/xml/cic.dtd b/plugins/xml/cic.dtd
index c8035cab9..c8035cab9 100644
--- a/contrib/xml/cic.dtd
+++ b/plugins/xml/cic.dtd
diff --git a/contrib/xml/cic2Xml.ml b/plugins/xml/cic2Xml.ml
index 08d3a8501..08d3a8501 100644
--- a/contrib/xml/cic2Xml.ml
+++ b/plugins/xml/cic2Xml.ml
diff --git a/contrib/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 13e5e6d5f..13e5e6d5f 100644
--- a/contrib/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
diff --git a/contrib/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index 17d1d5dab..17d1d5dab 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
diff --git a/contrib/xml/doubleTypeInference.mli b/plugins/xml/doubleTypeInference.mli
index 2e14b5580..2e14b5580 100644
--- a/contrib/xml/doubleTypeInference.mli
+++ b/plugins/xml/doubleTypeInference.mli
diff --git a/contrib/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 407f86b36..407f86b36 100644
--- a/contrib/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
diff --git a/contrib/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml
index f7524671f..f7524671f 100644
--- a/contrib/xml/proof2aproof.ml
+++ b/plugins/xml/proof2aproof.ml
diff --git a/contrib/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index a501fb6a6..a501fb6a6 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
diff --git a/contrib/xml/theoryobject.dtd b/plugins/xml/theoryobject.dtd
index 953fe0092..953fe0092 100644
--- a/contrib/xml/theoryobject.dtd
+++ b/plugins/xml/theoryobject.dtd
diff --git a/contrib/xml/unshare.ml b/plugins/xml/unshare.ml
index f30f8230d..f30f8230d 100644
--- a/contrib/xml/unshare.ml
+++ b/plugins/xml/unshare.ml
diff --git a/contrib/xml/unshare.mli b/plugins/xml/unshare.mli
index 31ba90372..31ba90372 100644
--- a/contrib/xml/unshare.mli
+++ b/plugins/xml/unshare.mli
diff --git a/contrib/xml/xml.ml4 b/plugins/xml/xml.ml4
index e2d04cb76..e2d04cb76 100644
--- a/contrib/xml/xml.ml4
+++ b/plugins/xml/xml.ml4
diff --git a/contrib/xml/xml.mli b/plugins/xml/xml.mli
index 3775287a5..3775287a5 100644
--- a/contrib/xml/xml.mli
+++ b/plugins/xml/xml.mli
diff --git a/contrib/xml/xml_plugin.mllib b/plugins/xml/xml_plugin.mllib
index 3297ff068..3297ff068 100644
--- a/contrib/xml/xml_plugin.mllib
+++ b/plugins/xml/xml_plugin.mllib
diff --git a/contrib/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 1ae186614..1ae186614 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
diff --git a/contrib/xml/xmlcommand.mli b/plugins/xml/xmlcommand.mli
index 66ff9f0bb..66ff9f0bb 100644
--- a/contrib/xml/xmlcommand.mli
+++ b/plugins/xml/xmlcommand.mli
diff --git a/contrib/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4
index 41c107ad2..41c107ad2 100644
--- a/contrib/xml/xmlentries.ml4
+++ b/plugins/xml/xmlentries.ml4
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 811a0db2c..919aacbbe 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -320,7 +320,7 @@ let include_dirs (inc_i,inc_r) =
   -I $(COQLIB)/proofs -I $(COQLIB)/tactics \\
   -I $(COQLIB)/toplevel";
     List.iter (fun c -> print " \\
-  -I $(COQLIB)/contrib/"; print c) Coq_config.contrib_dirs; print "\n";
+  -I $(COQLIB)/plugins/"; print c) Coq_config.plugins_dirs; print "\n";
     print "COQLIBS:="; print_list "\\\n  " str_i'; print " "; print_list "\\\n  " str_r; print "\n";
     print "COQDOCLIBS:=";   print_list "\\\n  " str_r; print "\n\n"
 
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 07c8126f1..f6acd0b65 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -167,11 +167,11 @@ let coqdep () =
   if not Coq_config.has_natdynlink then option_natdynlk := false;
   if !Flags.boot then begin
     add_rec_dir add_known "theories" ["Coq"];
-    add_rec_dir add_known "contrib" ["Coq"]
+    add_rec_dir add_known "plugins" ["Coq"]
   end else begin
     let coqlib = Envars.coqlib () in
     add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
-    add_rec_dir add_coqlib_known (coqlib//"contrib") ["Coq"];
+    add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
     add_dir add_coqlib_known (coqlib//"user-contrib") []
   end;
   List.iter (fun (f,d) -> add_mli_known f d) !mliAccu;
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 67113aa06..59fe701aa 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -12,8 +12,8 @@ open Coqdep_common
 
 (** [coqdep_boot] is a stripped-down version of [coqdep], whose
     behavior is the one of [coqdep -boot]. Its only dependencies
-    are [Coqdep_lexer] and [Unix], and it should stay so.
-    If it need someday some additional information, pass it via
+    are [Coqdep_lexer], [Coqdep_common] and [Unix], and it should stay so.
+    If it needs someday some additional information, pass it via
     options (see for instance [option_natdynlk] below).
 *)
 
@@ -29,7 +29,7 @@ let coqdep_boot () =
   if Array.length Sys.argv < 2 then exit 1;
   parse (List.tl (Array.to_list Sys.argv));
   add_rec_dir add_known "theories" ["Coq"];
-  add_rec_dir add_known "contrib" ["Coq"];
+  add_rec_dir add_known "plugins" ["Coq"];
   List.iter (fun (f,d) -> add_mli_known f d) !mliAccu;
   List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu;
   List.iter (fun (f,_,d) -> add_ml_known f d) !mlAccu;
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 90a36620a..e736fc676 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -97,11 +97,11 @@ let theories_dirs_map = [
 let init_load_path () =
   let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
-  let dirs = "states" :: ["contrib"] in
+  let dirs = ["states";"plugins"] in
     (* first user-contrib *)
     if Sys.file_exists user_contrib then 
       Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
-    (* then states, contrib and dev *)
+    (* then states, theories and dev *)
     List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
     (* developer specific directory to open *)
     if Coq_config.local then coq_add_path (coqlib/"dev") "dev";