[doc] [build] Remove ocamlbuild leftovers.

We had a brief leftovers of the ocamlbuild experiment that are not
relevant anymore as it was removed from the tree a few years ago.

p.s: The amount of cruft we have in the `dev/build/windows` folder is
staggering, see for example what `git grep ocamlbuild` returns.

5 files changed, 5 insertions, 38 deletions

diff --git a/.gitignore b/.gitignore
index 05869e2a0c..63da6b4d0e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -50,7 +50,6 @@ TAGS
 bin/
 _build_ci
 _build
-myocamlbuild_config.ml
 config/Makefile
 config/coq_config.ml
 config/coq_config.py
diff --git a/Makefile b/Makefile
index a15870faca..b74e4e5d4f 100644
--- a/Makefile
+++ b/Makefile
@@ -261,7 +261,7 @@ cacheclean:
 	find theories plugins test-suite -name '.*.aux' -exec rm -f {} +
 
 cleanconfig:
-	rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist
+	rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist
 
 distclean: clean cleanconfig cacheclean timingclean
 
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index fd3101613a..8cefe699cc 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -140,11 +140,9 @@ New files
 For a new file, in most cases, you just have to add it to the proper
 file list(s):
  - For .ml, in the corresponding .mllib (e.g. kernel/kernel.mllib)
-   These files are also used by the experimental ocamlbuild plugin,
-   which is quite touchy about them : be careful with order,
-   duplicated entries, whitespace errors, and do not mention .mli there.
-   If module B depends on module A, then B should be after A in the .mllib
-   file.
+   Be careful with order, duplicated entries, whitespace errors, and
+   do not mention .mli there.  If module B depends on module A, then B
+   should be after A in the .mllib file.
 - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
  - The definitions in Makefile.common might have to be adapted too.
  - If your file needs a specific rule, add it to Makefile.build
diff --git a/dev/doc/ocamlbuild.txt b/dev/doc/ocamlbuild.txt
deleted file mode 100644
index efedbc506e..0000000000
--- a/dev/doc/ocamlbuild.txt
+++ /dev/null
@@ -1,30 +0,0 @@
-Ocamlbuild & Coq
-----------------
-
-A quick note in case someone else gets interested someday in compiling
-Coq via ocamlbuild : such an experimental build system has existed
-in the past (more or less maintained from 2009 to 2013), in addition
-to the official build system via gnu make. But this build via
-ocamlbuild has been severly broken since early 2014 (and don't work
-in 8.5, for instance). This experiment has attracted very limited
-interest from other developers over the years, and has been quite
-cumbersome to maintain, so it is now officially discontinued.
-If you want to have a look at the files of this build system
-(especially myocamlbuild.ml), you can fetch :
- - my last effort at repairing this build system (up to coqtop.native) :
-   https://github.com/letouzey/coq-wip/tree/ocamlbuild-partial-repair
- - coq official v8.5 branch (recent but broken)
- - coq v8.4 branch(less up-to-date, but works).
-
-For the record, the three main drawbacks of this experiments were:
- - recurrent issues with circularities reported by ocamlbuild
-   (even though make was happy) during the evolution of Coq sources
- - no proper support of parallel build
- - quite slow re-traversal of already built things
-See the two corresponding bug reports on Mantis, or
-https://github.com/ocaml/ocamlbuild/issues/52
-
-As an interesting feature, I successfully used this to cross-compile
-Coq 8.4 from linux to win32 via mingw.
-
-Pierre Letouzey, june 2016
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index d91c4f0b34..7bb1390cad 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -46,7 +46,7 @@ let usage_coq_makefile () =
 \n\
 \n[file.v]: Coq file to be compiled\
 \n[file.ml[i4]?]: Objective Caml file to be compiled\
-\n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\
+\n[file.ml{lib,pack}]: ocamlbuild-style file that describes a Objective Caml\
 \n  library/module\
 \n[any] : subdirectory that should be \"made\" and has a Makefile itself\
 \n  to do so. Very fragile and discouraged.\