Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.

Reviewed-by: Zimmi48

4 files changed, 97 insertions, 99 deletions

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