108 files changed, 151 insertions, 137 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index a7c0846e35..888428d1f6 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -111,33 +111,48 @@
 ########## Plugins ##########
 
 /plugins/btauto/       @coq/btauto-maintainers
+/theories/btauto/      @coq/btauto-maintainers
 
 /plugins/cc/           @coq/cc-maintainers
+/theories/cc/          @coq/cc-maintainers
 
 /plugins/derive/       @coq/derive-maintainers
+/theories/derive/      @coq/derive-maintainers
 
 /plugins/extraction/   @coq/extraction-maintainers
+/theories/extraction/  @coq/extraction-maintainers
 
 /plugins/firstorder/   @coq/firstorder-maintainers
+/theories/firstorder/  @coq/firstorder-maintainers
 
 /plugins/funind/       @coq/funind-maintainers
+/theories/funind/      @coq/funind-maintainers
 
 /plugins/ltac/         @coq/ltac-maintainers
+/theories/ltac/        @coq/ltac-maintainers
 
 /plugins/micromega/    @coq/micromega-maintainers
+/theories/micromega/   @coq/micromega-maintainers
 /test-suite/micromega/ @coq/micromega-maintainers
 
 /plugins/nsatz/        @coq/nsatz-maintainers
+/theories/nsatz/       @coq/nsatz-maintainers
 
 /plugins/setoid_ring/  @coq/ring-maintainers
+/theories/setoid_ring/ @coq/ring-maintainers
 
 /plugins/ssrmatching/  @coq/ssreflect-maintainers
+/theories/ssrmatching/ @coq/ssreflect-maintainers
+
 /plugins/ssr/          @coq/ssreflect-maintainers
+/theories/ssr/         @coq/ssreflect-maintainers
+
 /test-suite/ssr/       @coq/ssreflect-maintainers
 
 /plugins/syntax/       @coq/parsing-maintainers
 
 /plugins/rtauto/       @coq/rtauto-maintainers
+/theories/rtauto/      @coq/rtauto-maintainers
 
 /user-contrib/Ltac2    @coq/ltac2-maintainers
 
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8fd5eb3972..4fdbe6e818 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -258,7 +258,7 @@ build:base:
   variables:
     COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
     # coqdoc for stdlib, until we know how to build it from installed Coq
-    EXTRA_TARGET: "stdlib"
+    EXTRA_TARGET: "doc-stdlib"
     EXTRA_INSTALL: "install-doc-stdlib-html install-doc-printable"
 
 # no coqide for 32bit: libgtk installation problems
diff --git a/Makefile.build b/Makefile.build
index 3c32e5bcc2..8a11d913a9 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -809,21 +809,20 @@ $(USERCONTRIBMLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter user-contrib/%, $(ML
 # NB: for make world, no need to mention explicitly the .cmxs of the plugins,
 # since they are all mentioned in at least one Declare ML Module in some .v
 
-coqlib: theories plugins
+coqlib: stdlib-vo contrib-vo
 ifdef QUICK
-	$(SHOW)'COQC -schedule-vio2vo $(NJOBS) theories/**.vio plugins/**.vio'
-	$(HIDE)$(BOOTCOQC) -schedule-vio2vo $(NJOBS) $(THEORIESVO) $(PLUGINSVO)
+	$(SHOW)'COQC -schedule-vio2vo $(NJOBS) theories/**.vio'
+	$(HIDE)$(BOOTCOQC) -schedule-vio2vo $(NJOBS) $(THEORIESVO) $(CONTRIBVO)
 endif
 
-coqlib.timing.diff: theories.timing.diff plugins.timing.diff
+coqlib.timing.diff: stdlib.timing.diff
 
-theories: $(THEORIESVO)
-plugins: $(PLUGINSVO)
+stdlib-vo: $(THEORIESVO)
+contrib-vo: $(CONTRIBVO)
 
-theories.timing.diff: $(THEORIESVO:.$(VO)=.v.timing.diff)
-plugins.timing.diff: $(PLUGINSVO:.$(VO)=.v.timing.diff)
+stdlib.timing.diff: $(ALLVO:.$(VO)=.v.timing.diff)
 
-.PHONY: coqlib theories plugins coqlib.timing.diff theories.timing.diff plugins.timing.diff
+.PHONY: coqlib stdlib-vo contrib-vo coqlib.timing.diff stdlib.timing.diff
 
 # The .vo files in Init are built with the -noinit option
 
diff --git a/Makefile.doc b/Makefile.doc
index 50c4acb416..eb58162cc0 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -56,9 +56,9 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
 ######################################################################
 
 .PHONY: doc doc-html doc-pdf doc-ps
-.PHONY: stdlib full-stdlib sphinx
+.PHONY: doc-stdlib full-stdlib sphinx
 
-doc: refman stdlib
+doc: refman doc-stdlib
 
 SPHINX_DEPS ?=
 ifndef QUICK
@@ -93,7 +93,7 @@ doc-pdf:\
 doc-ps:\
   doc/stdlib/Library.ps
 
-stdlib: \
+doc-stdlib: \
   doc/stdlib/html/index.html doc/stdlib/Library.ps doc/stdlib/Library.pdf
 
 full-stdlib: \
@@ -129,7 +129,7 @@ doc/unreleased.rst: $(wildcard doc/changelog/00-title.rst doc/changelog/*/*.rst)
 # Standard library
 ######################################################################
 
-DOCLIBS=-R theories Coq -R plugins Coq -Q user-contrib/Ltac2 Ltac2
+DOCLIBS=-R theories Coq -Q user-contrib/Ltac2 Ltac2
 
 ### Standard library (browsable html format)
 
diff --git a/Makefile.make b/Makefile.make
index e63a578e37..e020ffc5be 100644
--- a/Makefile.make
+++ b/Makefile.make
@@ -275,7 +275,7 @@ depclean:
 	find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} +
 
 cacheclean:
-	find theories plugins test-suite -name '.*.aux' -exec rm -f {} +
+	find theories test-suite -name '.*.aux' -exec rm -f {} +
 
 cleanconfig:
 	rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist
diff --git a/Makefile.vofiles b/Makefile.vofiles
index fe7ca7c36f..04bc2cf105 100644
--- a/Makefile.vofiles
+++ b/Makefile.vofiles
@@ -13,8 +13,8 @@ endif
 ###########################################################################
 
 THEORIESVO := $(patsubst %.v,%.$(VO),$(shell find theories -type f -name "*.v"))
-PLUGINSVO := $(patsubst %.v,%.$(VO),$(shell find plugins $(addprefix user-contrib/, $(USERCONTRIBDIRS)) -type f -name "*.v"))
-ALLVO := $(THEORIESVO) $(PLUGINSVO)
+CONTRIBVO := $(patsubst %.v,%.$(VO),$(shell find $(addprefix user-contrib/, $(USERCONTRIBDIRS)) -type f -name "*.v"))
+ALLVO := $(THEORIESVO) $(CONTRIBVO)
 VFILES := $(ALLVO:.$(VO)=.v)
 
 ## More specific targets
@@ -23,17 +23,15 @@ THEORIESLIGHTVO:= \
  $(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO))
 
 # convert a (stdlib) filename into a module name:
-# remove .vo, replace theories and plugins by Coq, and replace slashes by dots
-vo_to_mod = $(subst /,.,$(patsubst user-contrib/%,%,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=)))))
+# remove .vo, replace stdlib by Coq, and replace slashes by dots
+vo_to_mod = $(subst /,.,$(patsubst user-contrib/%,%,$(patsubst theories/%,Coq.%,$(1:.vo=))))
 
 ALLMODS:=$(call vo_to_mod,$(ALLVO:.$(VO)=.vo))
 
-
 # Converting a stdlib filename into native compiler filenames
 # Used for install targets
-vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%,N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*))))))
-
-vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%,N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o))))))
+vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%,N%, $(patsubst theories/%,NCoq_%,$(vo:.$(VO)=.cm*)))))
+vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%,N%, $(patsubst theories/%,NCoq_%,$(vo:.$(VO)=.o)))))
 
 ifdef QUICK
 GLOBFILES:=
diff --git a/doc/README.md b/doc/README.md
index ef3ccc2105..7fa6f5cf3d 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -96,7 +96,7 @@ Alternatively, you can use some specific targets:
 - `make refman-{html,pdf}`
   to produce only one format of the reference manual
 
-- `make stdlib`
+- `make doc-stdlib`
   to produce all formats of the Coq standard library
 
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 36a5916868..2fa4f1fa42 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -275,7 +275,7 @@ These patterns can be used when the hypothesis is an equality:
    :n:`or` has multiple constructors (:n:`or_introl` and :n:`or_intror`),
    while :n:`and` has a single constructor (:n:`conj`) with multiple parameters
    (:n:`A` and :n:`B`).
-   These are defined in theories/Init/Logic.v.  The "where" clauses define the
+   These are defined in ``theories/Init/Logic.v``.  The "where" clauses define the
    infix notation for "or" and "and".
 
    .. coqdoc::
diff --git a/doc/stdlib/dune b/doc/stdlib/dune
index 828caecabc..093c7a62b2 100644
--- a/doc/stdlib/dune
+++ b/doc/stdlib/dune
@@ -5,7 +5,6 @@
  (deps
    make-library-index index-list.html.template hidden-files
    (source_tree %{project_root}/theories)
-   (source_tree %{project_root}/plugins)
    (source_tree %{project_root}/user-contrib))
  (action
   (chdir %{project_root}
@@ -17,7 +16,6 @@
   (deps
    ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg
    (source_tree %{project_root}/theories)
-   (source_tree %{project_root}/plugins)
    (source_tree %{project_root}/user-contrib)
    (:header %{project_root}/doc/common/styles/html/coqremote/header.html)
    (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html)
@@ -26,7 +24,7 @@
  (action
   (progn
    (run mkdir -p html)
-   (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/plugins %{project_root}/user-contrib -name *.v)")
+   (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/user-contrib -name *.v)")
    (run mv html/index.html html/genindex.html)
    (with-stdout-to
      _index.html
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index dbc3a42ee9..60d6039b0f 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -1,90 +1,90 @@
-plugins/btauto/Algebra.v
-plugins/btauto/Btauto.v
-plugins/btauto/Reflect.v
-plugins/derive/Derive.v
-plugins/extraction/ExtrHaskellBasic.v
-plugins/extraction/ExtrHaskellNatInt.v
-plugins/extraction/ExtrHaskellNatInteger.v
-plugins/extraction/ExtrHaskellNatNum.v
-plugins/extraction/ExtrHaskellString.v
-plugins/extraction/ExtrHaskellZInt.v
-plugins/extraction/ExtrHaskellZInteger.v
-plugins/extraction/ExtrHaskellZNum.v
-plugins/extraction/ExtrOcamlBasic.v
-plugins/extraction/ExtrOcamlBigIntConv.v
-plugins/extraction/ExtrOcamlChar.v
-plugins/extraction/ExtrOCamlInt63.v
-plugins/extraction/ExtrOCamlFloats.v
-plugins/extraction/ExtrOcamlIntConv.v
-plugins/extraction/ExtrOcamlNatBigInt.v
-plugins/extraction/ExtrOcamlNatInt.v
-plugins/extraction/ExtrOcamlString.v
-plugins/extraction/ExtrOcamlNativeString.v
-plugins/extraction/ExtrOcamlZBigInt.v
-plugins/extraction/ExtrOcamlZInt.v
-plugins/extraction/Extraction.v
-plugins/funind/FunInd.v
-plugins/funind/Recdef.v
-plugins/ltac/Ltac.v
-plugins/micromega/Ztac.v
-plugins/micromega/DeclConstant.v
-plugins/micromega/Env.v
-plugins/micromega/EnvRing.v
-plugins/micromega/Fourier.v
-plugins/micromega/Fourier_util.v
-plugins/micromega/Lia.v
-plugins/micromega/Lqa.v
-plugins/micromega/Lra.v
-plugins/micromega/MExtraction.v
-plugins/micromega/OrderedRing.v
-plugins/micromega/Psatz.v
-plugins/micromega/QMicromega.v
-plugins/micromega/RMicromega.v
-plugins/micromega/Refl.v
-plugins/micromega/RingMicromega.v
-plugins/micromega/Tauto.v
-plugins/micromega/VarMap.v
-plugins/micromega/ZCoeff.v
-plugins/micromega/ZMicromega.v
-plugins/micromega/ZifyInst.v
-plugins/micromega/ZifyBool.v
-plugins/micromega/ZifyComparison.v
-plugins/micromega/ZifyClasses.v
-plugins/micromega/Zify.v
-plugins/nsatz/Nsatz.v
-plugins/omega/Omega.v
-plugins/omega/OmegaLemmas.v
-plugins/omega/OmegaPlugin.v
-plugins/omega/OmegaTactic.v
-plugins/omega/PreOmega.v
-plugins/quote/Quote.v
-plugins/romega/ROmega.v
-plugins/romega/ReflOmegaCore.v
-plugins/rtauto/Bintree.v
-plugins/rtauto/Rtauto.v
-plugins/setoid_ring/Algebra_syntax.v
-plugins/setoid_ring/ArithRing.v
-plugins/setoid_ring/BinList.v
-plugins/setoid_ring/Cring.v
-plugins/setoid_ring/Field.v
-plugins/setoid_ring/Field_tac.v
-plugins/setoid_ring/Field_theory.v
-plugins/setoid_ring/InitialRing.v
-plugins/setoid_ring/Integral_domain.v
-plugins/setoid_ring/NArithRing.v
-plugins/setoid_ring/Ncring.v
-plugins/setoid_ring/Ncring_initial.v
-plugins/setoid_ring/Ncring_polynom.v
-plugins/setoid_ring/Ncring_tac.v
-plugins/setoid_ring/RealField.v
-plugins/setoid_ring/Ring.v
-plugins/setoid_ring/Ring_base.v
-plugins/setoid_ring/Ring_polynom.v
-plugins/setoid_ring/Ring_tac.v
-plugins/setoid_ring/Ring_theory.v
-plugins/setoid_ring/Rings_Q.v
-plugins/setoid_ring/Rings_R.v
-plugins/setoid_ring/Rings_Z.v
-plugins/setoid_ring/ZArithRing.v
-plugins/ssr/ssrunder.v
-plugins/ssr/ssrsetoid.v
+theories/btauto/Algebra.v
+theories/btauto/Btauto.v
+theories/btauto/Reflect.v
+theories/derive/Derive.v
+theories/extraction/ExtrHaskellBasic.v
+theories/extraction/ExtrHaskellNatInt.v
+theories/extraction/ExtrHaskellNatInteger.v
+theories/extraction/ExtrHaskellNatNum.v
+theories/extraction/ExtrHaskellString.v
+theories/extraction/ExtrHaskellZInt.v
+theories/extraction/ExtrHaskellZInteger.v
+theories/extraction/ExtrHaskellZNum.v
+theories/extraction/ExtrOcamlBasic.v
+theories/extraction/ExtrOcamlBigIntConv.v
+theories/extraction/ExtrOcamlChar.v
+theories/extraction/ExtrOCamlInt63.v
+theories/extraction/ExtrOCamlFloats.v
+theories/extraction/ExtrOcamlIntConv.v
+theories/extraction/ExtrOcamlNatBigInt.v
+theories/extraction/ExtrOcamlNatInt.v
+theories/extraction/ExtrOcamlString.v
+theories/extraction/ExtrOcamlNativeString.v
+theories/extraction/ExtrOcamlZBigInt.v
+theories/extraction/ExtrOcamlZInt.v
+theories/extraction/Extraction.v
+theories/funind/FunInd.v
+theories/funind/Recdef.v
+theories/ltac/Ltac.v
+theories/micromega/Ztac.v
+theories/micromega/DeclConstant.v
+theories/micromega/Env.v
+theories/micromega/EnvRing.v
+theories/micromega/Fourier.v
+theories/micromega/Fourier_util.v
+theories/micromega/Lia.v
+theories/micromega/Lqa.v
+theories/micromega/Lra.v
+theories/micromega/MExtraction.v
+theories/micromega/OrderedRing.v
+theories/micromega/Psatz.v
+theories/micromega/QMicromega.v
+theories/micromega/RMicromega.v
+theories/micromega/Refl.v
+theories/micromega/RingMicromega.v
+theories/micromega/Tauto.v
+theories/micromega/VarMap.v
+theories/micromega/ZCoeff.v
+theories/micromega/ZMicromega.v
+theories/micromega/ZifyInst.v
+theories/micromega/ZifyBool.v
+theories/micromega/ZifyComparison.v
+theories/micromega/ZifyClasses.v
+theories/micromega/Zify.v
+theories/nsatz/Nsatz.v
+theories/omega/Omega.v
+theories/omega/OmegaLemmas.v
+theories/omega/OmegaPlugin.v
+theories/omega/OmegaTactic.v
+theories/omega/PreOmega.v
+theories/quote/Quote.v
+theories/romega/ROmega.v
+theories/romega/ReflOmegaCore.v
+theories/rtauto/Bintree.v
+theories/rtauto/Rtauto.v
+theories/setoid_ring/Algebra_syntax.v
+theories/setoid_ring/ArithRing.v
+theories/setoid_ring/BinList.v
+theories/setoid_ring/Cring.v
+theories/setoid_ring/Field.v
+theories/setoid_ring/Field_tac.v
+theories/setoid_ring/Field_theory.v
+theories/setoid_ring/InitialRing.v
+theories/setoid_ring/Integral_domain.v
+theories/setoid_ring/NArithRing.v
+theories/setoid_ring/Ncring.v
+theories/setoid_ring/Ncring_initial.v
+theories/setoid_ring/Ncring_polynom.v
+theories/setoid_ring/Ncring_tac.v
+theories/setoid_ring/RealField.v
+theories/setoid_ring/Ring.v
+theories/setoid_ring/Ring_base.v
+theories/setoid_ring/Ring_polynom.v
+theories/setoid_ring/Ring_tac.v
+theories/setoid_ring/Ring_theory.v
+theories/setoid_ring/Rings_Q.v
+theories/setoid_ring/Rings_R.v
+theories/setoid_ring/Rings_Z.v
+theories/setoid_ring/ZArithRing.v
+theories/ssr/ssrunder.v
+theories/ssr/ssrsetoid.v
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index b2ddf36b65..51688e2d9e 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -619,11 +619,11 @@ through the <tt>Require Import</tt> command.</p>
     small scale reflection formalization technique
   </dt>
   <dd>
-    plugins/ssrmatching/ssrmatching.v
-    plugins/ssr/ssrclasses.v
-    plugins/ssr/ssreflect.v
-    plugins/ssr/ssrbool.v
-    plugins/ssr/ssrfun.v
+    theories/ssrmatching/ssrmatching.v
+    theories/ssr/ssrclasses.v
+    theories/ssr/ssreflect.v
+    theories/ssr/ssrbool.v
+    theories/ssr/ssrfun.v
   </dd>
 
   <dt> <b>Ltac2</b>:
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index 732f15b78a..a51308f153 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -8,7 +8,7 @@ HIDDEN=$2
 cp -f $FILE.template tmp
 echo -n "Building file index-list.prehtml... "
 
-LIBDIRS=`find theories/* plugins/* user-contrib/* -type d ! -name .coq-native`
+LIBDIRS=`find theories/* user-contrib/* -type d ! -name .coq-native`
 
 for k in $LIBDIRS; do
     if [[ $k =~ "user-contrib" ]]; then
diff --git a/dune b/dune
index c91f824f3b..a3d596af48 100644
--- a/dune
+++ b/dune
@@ -27,9 +27,9 @@
   (source_tree user-contrib))
  (action
   (with-stdout-to .vfiles.d
-   (bash "%{bin:coqdep} -dyndep both -noglob -boot -R theories Coq -R plugins Coq -Q user-contrib/Ltac2 Ltac2 -I user-contrib/Ltac2 \
+   (bash "%{bin:coqdep} -dyndep both -noglob -boot -R theories Coq -Q user-contrib/Ltac2 Ltac2 -I user-contrib/Ltac2 \
           `find plugins/ -maxdepth 1 -mindepth 1 -type d -printf '-I %p '` \
-          `find theories plugins user-contrib -type f -name *.v`"))))
+          `find theories user-contrib -type f -name *.v`"))))
 
 (alias
  (name vodeps)
diff --git a/plugins/fourier/plugin_base.dune b/plugins/fourier/plugin_base.dune
deleted file mode 100644
index 8cc76f6f9e..0000000000
--- a/plugins/fourier/plugin_base.dune
+++ /dev/null
@@ -1,5 +0,0 @@
-(library
- (name fourier_plugin)
- (public_name coq.plugins.fourier)
- (synopsis "Coq's fourier plugin")
- (libraries coq.plugins.ltac))
diff --git a/plugins/btauto/Algebra.v b/theories/btauto/Algebra.v
index 4a603f2c52..4a603f2c52 100644
--- a/plugins/btauto/Algebra.v
+++ b/theories/btauto/Algebra.v
diff --git a/plugins/btauto/Btauto.v b/theories/btauto/Btauto.v
index d3331ccf89..d3331ccf89 100644
--- a/plugins/btauto/Btauto.v
+++ b/theories/btauto/Btauto.v
diff --git a/plugins/btauto/Reflect.v b/theories/btauto/Reflect.v
index 867fe69550..867fe69550 100644
--- a/plugins/btauto/Reflect.v
+++ b/theories/btauto/Reflect.v
diff --git a/plugins/derive/Derive.v b/theories/derive/Derive.v
index d1046ae79b..d1046ae79b 100644
--- a/plugins/derive/Derive.v
+++ b/theories/derive/Derive.v
diff --git a/plugins/extraction/ExtrHaskellBasic.v b/theories/extraction/ExtrHaskellBasic.v
index d08a81da64..d08a81da64 100644
--- a/plugins/extraction/ExtrHaskellBasic.v
+++ b/theories/extraction/ExtrHaskellBasic.v
diff --git a/plugins/extraction/ExtrHaskellNatInt.v b/theories/extraction/ExtrHaskellNatInt.v
index 267322d9ed..267322d9ed 100644
--- a/plugins/extraction/ExtrHaskellNatInt.v
+++ b/theories/extraction/ExtrHaskellNatInt.v
diff --git a/plugins/extraction/ExtrHaskellNatInteger.v b/theories/extraction/ExtrHaskellNatInteger.v
index 4c5c71f58a..4c5c71f58a 100644
--- a/plugins/extraction/ExtrHaskellNatInteger.v
+++ b/theories/extraction/ExtrHaskellNatInteger.v
diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/theories/extraction/ExtrHaskellNatNum.v
index 09b0444614..09b0444614 100644
--- a/plugins/extraction/ExtrHaskellNatNum.v
+++ b/theories/extraction/ExtrHaskellNatNum.v
diff --git a/plugins/extraction/ExtrHaskellString.v b/theories/extraction/ExtrHaskellString.v
index 8c61f4e96b..8c61f4e96b 100644
--- a/plugins/extraction/ExtrHaskellString.v
+++ b/theories/extraction/ExtrHaskellString.v
diff --git a/plugins/extraction/ExtrHaskellZInt.v b/theories/extraction/ExtrHaskellZInt.v
index 0345ffc4e8..0345ffc4e8 100644
--- a/plugins/extraction/ExtrHaskellZInt.v
+++ b/theories/extraction/ExtrHaskellZInt.v
diff --git a/plugins/extraction/ExtrHaskellZInteger.v b/theories/extraction/ExtrHaskellZInteger.v
index f7f9e2f80d..f7f9e2f80d 100644
--- a/plugins/extraction/ExtrHaskellZInteger.v
+++ b/theories/extraction/ExtrHaskellZInteger.v
diff --git a/plugins/extraction/ExtrHaskellZNum.v b/theories/extraction/ExtrHaskellZNum.v
index 4141bd203f..4141bd203f 100644
--- a/plugins/extraction/ExtrHaskellZNum.v
+++ b/theories/extraction/ExtrHaskellZNum.v
diff --git a/plugins/extraction/ExtrOCamlFloats.v b/theories/extraction/ExtrOCamlFloats.v
index 1891772cc2..1891772cc2 100644
--- a/plugins/extraction/ExtrOCamlFloats.v
+++ b/theories/extraction/ExtrOCamlFloats.v
diff --git a/plugins/extraction/ExtrOCamlInt63.v b/theories/extraction/ExtrOCamlInt63.v
index a2ee602313..a2ee602313 100644
--- a/plugins/extraction/ExtrOCamlInt63.v
+++ b/theories/extraction/ExtrOCamlInt63.v
diff --git a/plugins/extraction/ExtrOcamlBasic.v b/theories/extraction/ExtrOcamlBasic.v
index 2f82b24862..2f82b24862 100644
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ b/theories/extraction/ExtrOcamlBasic.v
diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/theories/extraction/ExtrOcamlBigIntConv.v
index f8bc86d087..f8bc86d087 100644
--- a/plugins/extraction/ExtrOcamlBigIntConv.v
+++ b/theories/extraction/ExtrOcamlBigIntConv.v
diff --git a/plugins/extraction/ExtrOcamlChar.v b/theories/extraction/ExtrOcamlChar.v
index 1e68365dd3..1e68365dd3 100644
--- a/plugins/extraction/ExtrOcamlChar.v
+++ b/theories/extraction/ExtrOcamlChar.v
diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/theories/extraction/ExtrOcamlIntConv.v
index 2de1906323..2de1906323 100644
--- a/plugins/extraction/ExtrOcamlIntConv.v
+++ b/theories/extraction/ExtrOcamlIntConv.v
diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/theories/extraction/ExtrOcamlNatBigInt.v
index a66d6e41fd..a66d6e41fd 100644
--- a/plugins/extraction/ExtrOcamlNatBigInt.v
+++ b/theories/extraction/ExtrOcamlNatBigInt.v
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/theories/extraction/ExtrOcamlNatInt.v
index 406a7f0d2b..406a7f0d2b 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/theories/extraction/ExtrOcamlNatInt.v
diff --git a/plugins/extraction/ExtrOcamlNativeString.v b/theories/extraction/ExtrOcamlNativeString.v
index ec3da1e444..ec3da1e444 100644
--- a/plugins/extraction/ExtrOcamlNativeString.v
+++ b/theories/extraction/ExtrOcamlNativeString.v
diff --git a/plugins/extraction/ExtrOcamlString.v b/theories/extraction/ExtrOcamlString.v
index 18c5ed3fe4..18c5ed3fe4 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/theories/extraction/ExtrOcamlString.v
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/theories/extraction/ExtrOcamlZBigInt.v
index c36ea50755..c36ea50755 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/theories/extraction/ExtrOcamlZBigInt.v
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/theories/extraction/ExtrOcamlZInt.v
index c7343d2468..c7343d2468 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/theories/extraction/ExtrOcamlZInt.v
diff --git a/plugins/extraction/Extraction.v b/theories/extraction/Extraction.v
index 207c95247e..207c95247e 100644
--- a/plugins/extraction/Extraction.v
+++ b/theories/extraction/Extraction.v
diff --git a/plugins/funind/FunInd.v b/theories/funind/FunInd.v
index d58b169154..d58b169154 100644
--- a/plugins/funind/FunInd.v
+++ b/theories/funind/FunInd.v
diff --git a/plugins/funind/Recdef.v b/theories/funind/Recdef.v
index cd3d69861f..cd3d69861f 100644
--- a/plugins/funind/Recdef.v
+++ b/theories/funind/Recdef.v
diff --git a/plugins/ltac/Ltac.v b/theories/ltac/Ltac.v
index e69de29bb2..e69de29bb2 100644
--- a/plugins/ltac/Ltac.v
+++ b/theories/ltac/Ltac.v
diff --git a/plugins/micromega/DeclConstant.v b/theories/micromega/DeclConstant.v
index 7ad5e313e3..7ad5e313e3 100644
--- a/plugins/micromega/DeclConstant.v
+++ b/theories/micromega/DeclConstant.v
diff --git a/plugins/micromega/Env.v b/theories/micromega/Env.v
index 8f4d4726b6..8f4d4726b6 100644
--- a/plugins/micromega/Env.v
+++ b/theories/micromega/Env.v
diff --git a/plugins/micromega/EnvRing.v b/theories/micromega/EnvRing.v
index 2762bb6b32..2762bb6b32 100644
--- a/plugins/micromega/EnvRing.v
+++ b/theories/micromega/EnvRing.v
diff --git a/plugins/micromega/Fourier.v b/theories/micromega/Fourier.v
index 0153de1dab..0153de1dab 100644
--- a/plugins/micromega/Fourier.v
+++ b/theories/micromega/Fourier.v
diff --git a/plugins/micromega/Fourier_util.v b/theories/micromega/Fourier_util.v
index 95fa5b88df..95fa5b88df 100644
--- a/plugins/micromega/Fourier_util.v
+++ b/theories/micromega/Fourier_util.v
diff --git a/plugins/micromega/Lia.v b/theories/micromega/Lia.v
index e53800d07d..e53800d07d 100644
--- a/plugins/micromega/Lia.v
+++ b/theories/micromega/Lia.v
diff --git a/plugins/micromega/Lqa.v b/theories/micromega/Lqa.v
index 25fb62cfad..25fb62cfad 100644
--- a/plugins/micromega/Lqa.v
+++ b/theories/micromega/Lqa.v
diff --git a/plugins/micromega/Lra.v b/theories/micromega/Lra.v
index 2403696696..2403696696 100644
--- a/plugins/micromega/Lra.v
+++ b/theories/micromega/Lra.v
diff --git a/plugins/micromega/MExtraction.v b/theories/micromega/MExtraction.v
index 0e8c09ef1b..0e8c09ef1b 100644
--- a/plugins/micromega/MExtraction.v
+++ b/theories/micromega/MExtraction.v
diff --git a/plugins/micromega/OrderedRing.v b/theories/micromega/OrderedRing.v
index d5884d9c1c..d5884d9c1c 100644
--- a/plugins/micromega/OrderedRing.v
+++ b/theories/micromega/OrderedRing.v
diff --git a/plugins/micromega/Psatz.v b/theories/micromega/Psatz.v
index 16ae24ba81..16ae24ba81 100644
--- a/plugins/micromega/Psatz.v
+++ b/theories/micromega/Psatz.v
diff --git a/plugins/micromega/QMicromega.v b/theories/micromega/QMicromega.v
index 4a02d1d01e..4a02d1d01e 100644
--- a/plugins/micromega/QMicromega.v
+++ b/theories/micromega/QMicromega.v
diff --git a/plugins/micromega/RMicromega.v b/theories/micromega/RMicromega.v
index 0f7a02c2c9..0f7a02c2c9 100644
--- a/plugins/micromega/RMicromega.v
+++ b/theories/micromega/RMicromega.v
diff --git a/plugins/micromega/Refl.v b/theories/micromega/Refl.v
index cd759029fa..cd759029fa 100644
--- a/plugins/micromega/Refl.v
+++ b/theories/micromega/Refl.v
diff --git a/plugins/micromega/RingMicromega.v b/theories/micromega/RingMicromega.v
index aa8876357a..aa8876357a 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/theories/micromega/RingMicromega.v
diff --git a/plugins/micromega/Tauto.v b/theories/micromega/Tauto.v
index a155207e2e..a155207e2e 100644
--- a/plugins/micromega/Tauto.v
+++ b/theories/micromega/Tauto.v
diff --git a/plugins/micromega/VarMap.v b/theories/micromega/VarMap.v
index 6db62e8401..6db62e8401 100644
--- a/plugins/micromega/VarMap.v
+++ b/theories/micromega/VarMap.v
diff --git a/plugins/micromega/ZCoeff.v b/theories/micromega/ZCoeff.v
index 08f3f39204..08f3f39204 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/theories/micromega/ZCoeff.v
diff --git a/plugins/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v
index 9bedb47371..9bedb47371 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/theories/micromega/ZMicromega.v
diff --git a/plugins/micromega/Zify.v b/theories/micromega/Zify.v
index 18cd196148..18cd196148 100644
--- a/plugins/micromega/Zify.v
+++ b/theories/micromega/Zify.v
diff --git a/plugins/micromega/ZifyBool.v b/theories/micromega/ZifyBool.v
index 4060478363..4060478363 100644
--- a/plugins/micromega/ZifyBool.v
+++ b/theories/micromega/ZifyBool.v
diff --git a/plugins/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v
index d3f7f91074..d3f7f91074 100644
--- a/plugins/micromega/ZifyClasses.v
+++ b/theories/micromega/ZifyClasses.v
diff --git a/plugins/micromega/ZifyComparison.v b/theories/micromega/ZifyComparison.v
index df75cf2c05..df75cf2c05 100644
--- a/plugins/micromega/ZifyComparison.v
+++ b/theories/micromega/ZifyComparison.v
diff --git a/plugins/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v
index edfb5a2a94..edfb5a2a94 100644
--- a/plugins/micromega/ZifyInst.v
+++ b/theories/micromega/ZifyInst.v
diff --git a/plugins/micromega/Ztac.v b/theories/micromega/Ztac.v
index 091f58a0ef..091f58a0ef 100644
--- a/plugins/micromega/Ztac.v
+++ b/theories/micromega/Ztac.v
diff --git a/plugins/nsatz/Nsatz.v b/theories/nsatz/Nsatz.v
index 896ee303cc..896ee303cc 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/theories/nsatz/Nsatz.v
diff --git a/plugins/omega/Omega.v b/theories/omega/Omega.v
index 4ceb530827..4ceb530827 100644
--- a/plugins/omega/Omega.v
+++ b/theories/omega/Omega.v
diff --git a/plugins/omega/OmegaLemmas.v b/theories/omega/OmegaLemmas.v
index d2378569fc..d2378569fc 100644
--- a/plugins/omega/OmegaLemmas.v
+++ b/theories/omega/OmegaLemmas.v
diff --git a/plugins/omega/OmegaPlugin.v b/theories/omega/OmegaPlugin.v
index 303eb0527a..303eb0527a 100644
--- a/plugins/omega/OmegaPlugin.v
+++ b/theories/omega/OmegaPlugin.v
diff --git a/plugins/omega/OmegaTactic.v b/theories/omega/OmegaTactic.v
index 303eb0527a..303eb0527a 100644
--- a/plugins/omega/OmegaTactic.v
+++ b/theories/omega/OmegaTactic.v
diff --git a/plugins/omega/PreOmega.v b/theories/omega/PreOmega.v
index 34533670f8..34533670f8 100644
--- a/plugins/omega/PreOmega.v
+++ b/theories/omega/PreOmega.v
diff --git a/plugins/rtauto/Bintree.v b/theories/rtauto/Bintree.v
index 6b92445326..6b92445326 100644
--- a/plugins/rtauto/Bintree.v
+++ b/theories/rtauto/Bintree.v
diff --git a/plugins/rtauto/Rtauto.v b/theories/rtauto/Rtauto.v
index 2e9b4347b9..2e9b4347b9 100644
--- a/plugins/rtauto/Rtauto.v
+++ b/theories/rtauto/Rtauto.v
diff --git a/plugins/setoid_ring/Algebra_syntax.v b/theories/setoid_ring/Algebra_syntax.v
index 5f594d29cd..5f594d29cd 100644
--- a/plugins/setoid_ring/Algebra_syntax.v
+++ b/theories/setoid_ring/Algebra_syntax.v
diff --git a/plugins/setoid_ring/ArithRing.v b/theories/setoid_ring/ArithRing.v
index 727e99f0b4..727e99f0b4 100644
--- a/plugins/setoid_ring/ArithRing.v
+++ b/theories/setoid_ring/ArithRing.v
diff --git a/plugins/setoid_ring/BinList.v b/theories/setoid_ring/BinList.v
index 958832274b..958832274b 100644
--- a/plugins/setoid_ring/BinList.v
+++ b/theories/setoid_ring/BinList.v
diff --git a/plugins/setoid_ring/Cring.v b/theories/setoid_ring/Cring.v
index df0313a624..df0313a624 100644
--- a/plugins/setoid_ring/Cring.v
+++ b/theories/setoid_ring/Cring.v
diff --git a/plugins/setoid_ring/Field.v b/theories/setoid_ring/Field.v
index 9ff07948df..9ff07948df 100644
--- a/plugins/setoid_ring/Field.v
+++ b/theories/setoid_ring/Field.v
diff --git a/plugins/setoid_ring/Field_tac.v b/theories/setoid_ring/Field_tac.v
index a5390efc7f..a5390efc7f 100644
--- a/plugins/setoid_ring/Field_tac.v
+++ b/theories/setoid_ring/Field_tac.v
diff --git a/plugins/setoid_ring/Field_theory.v b/theories/setoid_ring/Field_theory.v
index 3736bc47a5..3736bc47a5 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/theories/setoid_ring/Field_theory.v
diff --git a/plugins/setoid_ring/InitialRing.v b/theories/setoid_ring/InitialRing.v
index dc096554c8..dc096554c8 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/theories/setoid_ring/InitialRing.v
diff --git a/plugins/setoid_ring/Integral_domain.v b/theories/setoid_ring/Integral_domain.v
index f1394c51d5..f1394c51d5 100644
--- a/plugins/setoid_ring/Integral_domain.v
+++ b/theories/setoid_ring/Integral_domain.v
diff --git a/plugins/setoid_ring/NArithRing.v b/theories/setoid_ring/NArithRing.v
index 8cda4ad714..8cda4ad714 100644
--- a/plugins/setoid_ring/NArithRing.v
+++ b/theories/setoid_ring/NArithRing.v
diff --git a/plugins/setoid_ring/Ncring.v b/theories/setoid_ring/Ncring.v
index 8f3de26272..8f3de26272 100644
--- a/plugins/setoid_ring/Ncring.v
+++ b/theories/setoid_ring/Ncring.v
diff --git a/plugins/setoid_ring/Ncring_initial.v b/theories/setoid_ring/Ncring_initial.v
index e40ef6056d..e40ef6056d 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/theories/setoid_ring/Ncring_initial.v
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/theories/setoid_ring/Ncring_polynom.v
index 048c8eecf9..048c8eecf9 100644
--- a/plugins/setoid_ring/Ncring_polynom.v
+++ b/theories/setoid_ring/Ncring_polynom.v
diff --git a/plugins/setoid_ring/Ncring_tac.v b/theories/setoid_ring/Ncring_tac.v
index 65233873b1..65233873b1 100644
--- a/plugins/setoid_ring/Ncring_tac.v
+++ b/theories/setoid_ring/Ncring_tac.v
diff --git a/plugins/setoid_ring/RealField.v b/theories/setoid_ring/RealField.v
index d83fcf3781..d83fcf3781 100644
--- a/plugins/setoid_ring/RealField.v
+++ b/theories/setoid_ring/RealField.v
diff --git a/plugins/setoid_ring/Ring.v b/theories/setoid_ring/Ring.v
index 35e308565f..35e308565f 100644
--- a/plugins/setoid_ring/Ring.v
+++ b/theories/setoid_ring/Ring.v
diff --git a/plugins/setoid_ring/Ring_base.v b/theories/setoid_ring/Ring_base.v
index 36e7890fbb..36e7890fbb 100644
--- a/plugins/setoid_ring/Ring_base.v
+++ b/theories/setoid_ring/Ring_base.v
diff --git a/plugins/setoid_ring/Ring_polynom.v b/theories/setoid_ring/Ring_polynom.v
index 092114ff0b..092114ff0b 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/theories/setoid_ring/Ring_polynom.v
diff --git a/plugins/setoid_ring/Ring_tac.v b/theories/setoid_ring/Ring_tac.v
index 0a14c0ee5c..0a14c0ee5c 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/theories/setoid_ring/Ring_tac.v
diff --git a/plugins/setoid_ring/Ring_theory.v b/theories/setoid_ring/Ring_theory.v
index dc45853458..dc45853458 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/theories/setoid_ring/Ring_theory.v
diff --git a/plugins/setoid_ring/Rings_Q.v b/theories/setoid_ring/Rings_Q.v
index b3ed0be916..b3ed0be916 100644
--- a/plugins/setoid_ring/Rings_Q.v
+++ b/theories/setoid_ring/Rings_Q.v
diff --git a/plugins/setoid_ring/Rings_R.v b/theories/setoid_ring/Rings_R.v
index ec91fa9e97..ec91fa9e97 100644
--- a/plugins/setoid_ring/Rings_R.v
+++ b/theories/setoid_ring/Rings_R.v
diff --git a/plugins/setoid_ring/Rings_Z.v b/theories/setoid_ring/Rings_Z.v
index 8a51bcea02..8a51bcea02 100644
--- a/plugins/setoid_ring/Rings_Z.v
+++ b/theories/setoid_ring/Rings_Z.v
diff --git a/plugins/setoid_ring/ZArithRing.v b/theories/setoid_ring/ZArithRing.v
index 833e19a698..833e19a698 100644
--- a/plugins/setoid_ring/ZArithRing.v
+++ b/theories/setoid_ring/ZArithRing.v
diff --git a/plugins/ssr/ssrbool.v b/theories/ssr/ssrbool.v
index 475859fcc2..475859fcc2 100644
--- a/plugins/ssr/ssrbool.v
+++ b/theories/ssr/ssrbool.v
diff --git a/plugins/ssr/ssrclasses.v b/theories/ssr/ssrclasses.v
index 0ae3f8c6a5..0ae3f8c6a5 100644
--- a/plugins/ssr/ssrclasses.v
+++ b/theories/ssr/ssrclasses.v
diff --git a/plugins/ssr/ssreflect.v b/theories/ssr/ssreflect.v
index bc4a57dedd..bc4a57dedd 100644
--- a/plugins/ssr/ssreflect.v
+++ b/theories/ssr/ssreflect.v
diff --git a/plugins/ssr/ssrfun.v b/theories/ssr/ssrfun.v
index dd847169b9..dd847169b9 100644
--- a/plugins/ssr/ssrfun.v
+++ b/theories/ssr/ssrfun.v
diff --git a/plugins/ssr/ssrsetoid.v b/theories/ssr/ssrsetoid.v
index 7c5cd135fe..7c5cd135fe 100644
--- a/plugins/ssr/ssrsetoid.v
+++ b/theories/ssr/ssrsetoid.v
diff --git a/plugins/ssr/ssrunder.v b/theories/ssr/ssrunder.v
index 7c529a6133..7c529a6133 100644
--- a/plugins/ssr/ssrunder.v
+++ b/theories/ssr/ssrunder.v
diff --git a/plugins/ssrmatching/ssrmatching.v b/theories/ssrmatching/ssrmatching.v
index 23a16615f5..23a16615f5 100644
--- a/plugins/ssrmatching/ssrmatching.v
+++ b/theories/ssrmatching/ssrmatching.v
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index f62947ec67..96fb9710c7 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -213,7 +213,7 @@ let record_dune d ff =
   if Sys.file_exists sd && Sys.is_directory sd then
     let out = open_out (bpath [sd;"dune"]) in
     let fmt = formatter_of_out_channel out in
-    if List.nth d 0 = "plugins" || List.nth d 0 = "user-contrib" then
+    if Sys.file_exists (bpath [sd; "plugin_base.dune"]) then
       fprintf fmt "(include plugin_base.dune)@\n";
     out_install fmt d ff;
     List.iter (pp_dep d fmt) ff;
@@ -285,8 +285,11 @@ let exec_ifile f =
     begin try
       let ic = open_in in_file in
       (try f ic
-       with _ -> eprintf "Error: exec_ifile@\n%!"; close_in ic)
-      with _ -> eprintf "Error: cannot open input file %s@\n%!" in_file
+       with exn ->
+         eprintf "Error: exec_ifile @[%s@]@\n%!" (Printexc.to_string exn);
+         close_in ic)
+      with _ ->
+        eprintf "Error: cannot open input file %s@\n%!" in_file
     end
   | _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1
 
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index ac348b9646..b353f8aff1 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -59,6 +59,12 @@ let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml =
     path_spec = VoPath { unix_path; coq_path ; has_ml = add_ml; implicit = load_init }
   }
 
+let build_stdlib_ml_path ~dir =
+  let open Loadpath in
+  { recursive = true
+  ; path_spec = MlPath dir
+  }
+
 let build_userlib_path ~unix_path =
   let open Loadpath in
   { recursive = true;
@@ -100,9 +106,9 @@ let libs_init_load_path ~load_init =
                            has_ml = AddTopML }
     } ] @
 
-  (* then standard library and plugins *)
-  [build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false;
-   build_stdlib_path ~load_init ~unix_path:(coqlib/"plugins")  ~coq_path ~with_ml:true ] @
+  (* then standard library *)
+  [build_stdlib_ml_path ~dir:(coqlib/"plugins")] @
+  [build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false] @
 
   (* then user-contrib *)
   (if Sys.file_exists user_contrib then