Merge branch 'yet-another-makefile-bigbang' into trunk

18 files changed, 204 insertions, 170 deletions

diff --git a/Makefile b/Makefile
index c5415d9f6..17ff8041f 100644
--- a/Makefile
+++ b/Makefile
@@ -63,15 +63,10 @@ define findx
  $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -exec $(2) {} \; | sed 's|^\./||')
 endef
 
-# We now discriminate .ml4 files according to their need of grammar.cma
-# or q_constr.cmo
-USEGRAMMAR := '(\*.*camlp4deps.*grammar'
-
 ## Files in the source tree
 
 LEXFILES := $(call find, '*.mll')
 export MLLIBFILES := $(call find, '*.mllib')
-export ML4BASEFILES := $(call findx, '*.ml4', grep -L -e $(USEGRAMMAR))
 export ML4FILES := $(call find, '*.ml4')
 export CFILES := $(call find, '*.c')
 
@@ -150,10 +145,7 @@ endif
 
 MAKE_OPTS := --warn-undefined-variable --no-builtin-rules
 
-GRAM_TARGETS := grammar/grammar.cma grammar/q_constr.cmo
-
 submake:
-	$(MAKE) $(MAKE_OPTS) -f Makefile.build BUILDGRAMMAR=1 $(GRAM_TARGETS)
 	$(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS)
 
 noconfig:
diff --git a/Makefile.build b/Makefile.build
index 190a62d00..18b1e4fb4 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -25,29 +25,23 @@ world: revision coq coqide documentation
 include Makefile.common
 include Makefile.doc
 
-# In a first phase, we restrict to the basic .ml4 (the ones without grammar.cma)
+MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
+DEPENDENCIES := \
+ $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(CFILES) $(VFILES))
 
-ifdef BUILDGRAMMAR
- MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4BASEFILES:.ml4=.ml)
- CURFILES := $(MLFILES) $(MLIFILES) $(ML4BASEFILES) grammar/grammar.mllib
-else
- MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
- CURFILES := $(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(CFILES) $(VFILES)
-endif
+# This include below will lauch the build of all concerned .d.
+# The - at front is for disabling warnings about currently missing ones.
+# For creating the missing .d, make will recursively build things like
+# coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d).
 
-CURDEPS:=$(addsuffix .d, $(CURFILES))
+-include $(DEPENDENCIES)
 
 # All dependency includes must be declared secondary, otherwise make will
 # delete them if it decided to build them by dependency instead of because
 # of include, and they will then be automatically deleted, leading to an
 # infinite loop.
 
-.SECONDARY: $(CURDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml)
-
-# This include below will lauch the build of all concerned .d.
-# The - at front is for disabling warnings about currently missing ones.
-
--include $(CURDEPS)
+.SECONDARY: $(DEPENDENCIES) $(GENFILES) $(ML4FILES:.ml4=.ml)
 
 
 ###########################################################################
@@ -117,7 +111,7 @@ $(if $(findstring $@,$(PRIVATEBINARIES)),\
 $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
 endef
 
-CAMLP4DEPS=$(shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $(1) \#))
+CAMLP4DEPS:=tools/compat5.cmo grammar/grammar.cma grammar/q_constr.cmo
 ifeq ($(CAMLP4),camlp5)
 CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
 else
@@ -139,7 +133,6 @@ else
 P4CMA:=camlp4lib.cma
 endif
 
-
 ###########################################################################
 # Infrastructure for the rest of the Makefile
 ###########################################################################
@@ -203,6 +196,74 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h
 	sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' $< | \
 	awk -f kernel/make-opcodes $(TOTARGET)
 
+
+###########################################################################
+#  grammar/grammar.cma
+###########################################################################
+
+## In this part, we compile grammar/grammar.cma (and grammar/q_constr.cmo)
+## without relying on .d dependency files, for bootstraping the creation
+## and inclusion of these .d files
+
+## Explicit dependencies for grammar stuff
+
+GRAMBASEDEPS := grammar/gramCompat.cmo grammar/q_util.cmi
+GRAMCMO := \
+ grammar/gramCompat.cmo grammar/q_util.cmo \
+ grammar/argextend.cmo grammar/tacextend.cmo grammar/vernacextend.cmo
+
+grammar/q_util.cmi : grammar/gramCompat.cmo
+grammar/argextend.cmo : $(GRAMBASEDEPS)
+grammar/q_constr.cmo : $(GRAMBASEDEPS)
+grammar/q_util.cmo : $(GRAMBASEDEPS)
+grammar/tacextend.cmo : $(GRAMBASEDEPS) grammar/argextend.cmo
+grammar/vernacextend.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo \
+ grammar/argextend.cmo
+
+## Ocaml compiler with the right options and -I for grammar
+
+GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \
+ -I $(MYCAMLP4LIB) -I grammar
+
+## Specific rules for grammar.cma
+
+grammar/grammar.cma : $(GRAMCMO)
+	$(SHOW)'Testing $@'
+	@touch test.mlp
+	$(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl test.mlp -o test.ml
+	$(HIDE)$(GRAMC) test.ml -o test-grammar
+	@rm -f test-grammar test.*
+	$(SHOW)'OCAMLC -a $@'   
+	$(HIDE)$(GRAMC) $^ -linkall -a -o $@
+
+## Support of Camlp5 and Camlp5
+
+# NB: compatibility modules for camlp4:
+# - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded
+# - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with
+#    syntax such that VERNAC EXTEND, we only load it in grammar/
+
+ifeq ($(CAMLP4),camlp4)
+ COMPATCMO:=tools/compat5.cmo tools/compat5b.cmo
+ GRAMP4USE:=$(COMPATCMO) -D$(CAMLVERSION)
+ GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl
+else
+ COMPATCMO:=
+ GRAMP4USE:=$(COMPATCMO) pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
+ GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl
+endif
+
+## Rules for standard .mlp and .mli files in grammar/
+
+grammar/%.cmo: grammar/%.mlp | $(COMPATCMO)
+	$(SHOW)'OCAMLC -c -pp $<'
+	$(HIDE)$(GRAMC) -c -pp '$(GRAMPP)' -impl $<
+
+grammar/%.cmi: grammar/%.mli
+	$(SHOW)'OCAMLC -c $<'
+	$(HIDE)$(GRAMC) -c $<
+
+
 ###########################################################################
 # Main targets (coqmktop, coqtop.opt, coqtop.byte)
 ###########################################################################
@@ -608,16 +669,26 @@ tools: $(TOOLS) $(DEBUGPRINTERS) $(OCAMLLIBDEP)
 # coqdep_boot : a basic version of coqdep, with almost no dependencies.
 
 # Here it is important to mention .ml files instead of .cmo in order
-# to avoid using implicit rules and hence .ml.d files that would need
-# coqdep_boot.
+# to avoid using implicit rules : at the time coqdep_boot is being built,
+# some .ml.d files may still be missing or not taken in account yet by make.
 
-OCAMLLIBDEPSRC:= tools/ocamllibdep.ml
+COQDEPBOOTSRC := \
+ lib/minisys.ml \
+ tools/coqdep_lexer.mli tools/coqdep_lexer.ml \
+ tools/coqdep_common.mli tools/coqdep_common.ml \
+ tools/coqdep_boot.ml
 
-$(OCAMLLIBDEP): $(OCAMLLIBDEPSRC)
+$(COQDEPBOOT): $(COQDEPBOOTSRC)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I tools, unix)
 
-# the full coqdep
+# Same for ocamllibdep
+
+$(OCAMLLIBDEP): tools/ocamllibdep.ml
+	$(SHOW)'OCAMLBEST -o $@'
+	$(HIDE)$(call bestocaml, -I tools, unix)
+
+# The full coqdep (unused by this build, but distributed by make install)
 
 $(COQDEP): $(patsubst %.cma,%$(BESTLIB),$(COQDEPCMO:.cmo=$(BESTOBJ)))
 	$(SHOW)'OCAMLBEST -o $@'
@@ -671,8 +742,6 @@ tools/compat5b.cmo: tools/compat5b.mlp
 else
 tools/compat5.cmo: tools/compat5.ml
 	$(OCAMLC) -c $<
-tools/compat5b.cmo: tools/compat5b.ml
-	$(OCAMLC) -c $<
 endif
 
 ###########################################################################
@@ -891,15 +960,6 @@ dev/printers.cma: | dev/printers.mllib.d
 	$(SHOW)'OCAMLC -a $@'   
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $^ -linkall -a -o $@
 
-grammar/grammar.cma: | grammar/grammar.mllib.d
-	$(SHOW)'Testing $@'
-	@touch test.ml4
-	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $^ -impl test.ml4 -o test.ml
-	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) test.ml -o test-grammar
-	@rm -f test-grammar test.*
-	$(SHOW)'OCAMLC -a $@'   
-	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $^ -linkall -a -o $@
-
 ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
 	$(SHOW)'CAMLP4O   $<'
 	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@
@@ -1029,15 +1089,10 @@ plugins/%_mod.ml: plugins/%.mllib
 	$(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@
 	$(HIDE)echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@
 
-# NB: compatibility modules for camlp4: 
-# - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded
-# - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with
-#    syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps
-
-%.ml: %.ml4 | %.ml4.d tools/compat5.cmo tools/compat5b.cmo
+%.ml: %.ml4 | $(CAMLP4DEPS)
 	$(SHOW)'CAMLP4O   $<'
-	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) tools/compat5.cmo \
-	  $(call CAMLP4DEPS,$<) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@
+	$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) \
+	  $(CAMLP4DEPS) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@
 
 %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d
 	$(SHOW)'COQC      $<'
@@ -1053,13 +1108,6 @@ endif
 # Dependencies
 ###########################################################################
 
-# .ml4.d contains the dependencies to generate the .ml from the .ml4
-# NOT to generate object code.
-
-%.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4
-	$(SHOW)'CAMLP4DEPS $<'
-	$(HIDE)echo "$*.ml: $(if $(NO_RECOMPILE_ML4),$(ORDER_ONLY_SEP)) $(call CAMLP4DEPS,$<)" $(TOTARGET)
-
 # Since OCaml 3.12.1, we could use again ocamldep directly, thanks to
 # the option -ml-synonym
 
@@ -1093,9 +1141,9 @@ dev/%.mllib.d: $(D_DEPEND_BEFORE_SRC) dev/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLL
 	$(SHOW)'OCAMLLIBDEP  $<'
 	$(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET)
 
-%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEP) $(GENVFILES)
+%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES)
 	$(SHOW)'COQDEP    $<'
-	$(HIDE)$(COQDEP) -boot $(DEPNATDYN) "$<" $(TOTARGET)
+	$(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET)
 
 %_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC)
 	$(SHOW)'CCDEP	$<'
diff --git a/Makefile.common b/Makefile.common
index e7d092876..5bf49ed76 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -63,7 +63,7 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 CORESRCDIRS:=\
   config 	lib		kernel		kernel/byterun	library \
   proofs 	tactics 	pretyping	interp		stm \
-  toplevel	parsing	printing	grammar	        intf	engine	ltac
+  toplevel	parsing 	printing	intf	engine	ltac
 
 PLUGINS:=\
   omega		romega 		micromega 	quote \
@@ -85,6 +85,7 @@ CHKSRCDIRS:= config lib checker
 ###########################################################################
 
 COQDEP:=bin/coqdep$(EXE)
+COQDEPBOOT:=bin/coqdep_boot$(EXE)
 OCAMLLIBDEP:=bin/ocamllibdep$(EXE)
 COQMAKEFILE:=bin/coq_makefile$(EXE)
 GALLINA:=bin/gallina$(EXE)
@@ -258,7 +259,7 @@ CSDPCERTCMO:=$(addprefix plugins/micromega/, \
 
 DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma
 
-COQDEPCMO:=$(COQENVCMO) lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo
+COQDEPCMO:=$(COQENVCMO) lib/minisys.cmo lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo
 
 COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \
   cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo )
diff --git a/checker/check.mllib b/checker/check.mllib
index a093fd959..2fa4d5797 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -39,6 +39,7 @@ CEphemeron
 Future
 CUnix
 
+Minisys
 System
 Profile
 RemoteCounter
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index af1120e97..fefcb0937 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -30,6 +30,11 @@ HISTORY:
     restricted set of .ml4 (see variable BUILDGRAMMAR).
   - then on the true target asked by the user.
 
+* June 2016 (Pierre Letouzey)
+  The files in grammar/ are now self-contained, we could compile
+  grammar.cma (and q_constr.cmo) directly, no need for a separate
+  subcall to make nor awkward include-failed-and-retry.
+
     
 ---------------------------------------------------------------------------
 
@@ -59,29 +64,14 @@ Cons:
 Makefiles hierachy
 ------------------
 
-Le Makefile a été séparé en plusieurs fichiers :
-
-- Makefile: coquille vide qui lançant Makefile.build sauf pour
-  clean et quelques petites choses ne nécessitant par de calculs
-  de dépendances.
-- Makefile.common : définitions des variables (essentiellement des
-  listes de fichiers)
-- Makefile.build : contient les regles de compilation, ainsi que
-  le "include" des dépendances (restreintes ou non selon la variable
-  BUILDGRAMMAR).
-- Makefile.doc : regles specifiques à la compilation de la documentation.
-
-
-Parallélisation
----------------
+The Makefile is separated in several files :
 
-Il y a actuellement un double appel interne à "make -f Makefile.build",
-d'abord pour construire grammar.cma/q_constr.cmo, puis le reste.
-Cela signifie que ce makefile est un petit peu moins parallélisable
-que strictement possible en théorie: par exemple, certaines choses
-faites lors du second make pourraient être faites en parallèle avec
-le premier. En pratique, ce premier make va suffisemment vite pour
-que cette limitation soit peu gênante.
+- Makefile: wrapper that triggers a call to Makefile.build, except for
+  clean and a few other little things doable without dependency analysis.
+- Makefile.common : variable definitions (mostly lists of files or
+  directories)
+- Makefile.build : contains compilation rules, and the "include" of dependencies
+- Makefile.doc : specific rules for compiling the documentation.
 
 
 FIND_VCS_CLAUSE
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 31d9875ad..4593a6ad5 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -113,15 +113,20 @@ Targets for cleaning various parts:
 
  - docclean: clean documentation
 
-.ml4 files
-----------
+.ml4/.mlp files
+---------------
 
-If a .ml4 file uses a grammar extension from Coq (such as grammar.cma
-or q_constr.cmo), it must contain a line like:
+There is now two kinds of preprocessed files : 
+ - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp)
+ - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
+   except coqide_main.ml4 and its specific rule
+
+This classification replaces the old mechanism of declaring the use
+of a grammar extension via a line of the form:
  (*i camlp4deps: "grammar.cma q_constr.cmo" i*)
 
 The use of (*i camlp4use: ... i*) to mention uses of standard
-extension such as IFDEF has been discontinued, the Makefile now
+extension such as IFDEF has also been discontinued, the Makefile now
 always calls camlp4 with pa_macros.cmo and a few others by default.
 
 For debugging a Coq grammar extension, it could be interesting
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 0957197cc..74b42842c 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -40,6 +40,7 @@ Unicode
 Errors
 Bigint
 CUnix
+Minisys
 System
 Envars
 Aux_file
diff --git a/grammar/argextend.ml4 b/grammar/argextend.mlp
index 8e06adce9..eaaa7f025 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.mlp
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
 open Q_util
 open GramCompat
 
diff --git a/grammar/gramCompat.ml4 b/grammar/gramCompat.mlp
index 6246da7bb..6246da7bb 100644
--- a/grammar/gramCompat.ml4
+++ b/grammar/gramCompat.mlp
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.mlp
index af90f5f2a..8e1587ec3 100644
--- a/grammar/q_constr.ml4
+++ b/grammar/q_constr.mlp
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
 open Q_util
 open GramCompat
 open Pcaml
diff --git a/grammar/q_util.ml4 b/grammar/q_util.mlp
index 2d5c40894..2d5c40894 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.mlp
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.mlp
index ae6d2d18e..ac6a7ac7f 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.mlp
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
 (** Implementation of the TACTIC EXTEND macro. *)
 
 open Q_util
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.mlp
index 215d27dbd..ce0431889 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.mlp
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
 (** Implementation of the VERNAC EXTEND macro. *)
 
 open Q_util
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 2be435f6f..a6c09058d 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -3,6 +3,7 @@ Bigint
 Segmenttree
 Unicodetable
 Unicode
+Minisys
 System
 CThread
 Spawn
diff --git a/lib/minisys.ml b/lib/minisys.ml
new file mode 100644
index 000000000..25e4d79c4
--- /dev/null
+++ b/lib/minisys.ml
@@ -0,0 +1,74 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Minisys regroups some code that used to be in System.
+    Unlike System, this module has no dependency and could
+    be used for initial compilation target such as coqdep_boot.
+    The functions here are still available in System thanks to
+    an include. For the signature, look at the top of system.mli
+*)
+
+(** Dealing with directories *)
+
+type unix_path = string (* path in unix-style, with '/' separator *)
+
+type file_kind =
+  | FileDir of unix_path * (* basename of path: *) string
+  | FileRegular of string (* basename of file *)
+
+(* Copy of Filename.concat but assuming paths to always be POSIX *)
+
+let (//) dirname filename =
+  let l = String.length dirname in
+  if l = 0 || dirname.[l-1] = '/'
+  then dirname ^ filename
+  else dirname ^ "/" ^ filename
+
+(* Excluding directories; We avoid directories starting with . as well
+   as CVS and _darcs and any subdirs given via -exclude-dir *)
+
+let skipped_dirnames = ref ["CVS"; "_darcs"]
+
+let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames
+
+let ok_dirname f =
+  not (f = "") && f.[0] != '.' &&
+  not (List.mem f !skipped_dirnames) (*&&
+  (match Unicode.ident_refutation f with None -> true | _ -> false)*)
+
+(* Check directory can be opened *)
+
+let exists_dir dir =
+  try Sys.is_directory dir with Sys_error _ -> false
+
+let check_unix_dir warn dir =
+  if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") &&
+    (String.length dir > 2 && dir.[1] = ':' ||
+     String.contains dir '\\' ||
+     String.contains dir ';')
+  then warn ("assuming " ^ dir ^
+             " to be a Unix path even if looking like a Win32 path.")
+
+let apply_subdir f path name =
+  (* we avoid all files and subdirs starting by '.' (e.g. .svn) *)
+  (* as well as skipped files like CVS, ... *)
+  if ok_dirname name then
+    let path = if path = "." then name else path//name in
+    match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with
+    | Unix.S_DIR -> f (FileDir (path,name))
+    | Unix.S_REG -> f (FileRegular name)
+    | _ -> ()
+
+let readdir dir = try Sys.readdir dir with any -> [||]
+
+let process_directory f path =
+  Array.iter (apply_subdir f path) (readdir path)
+
+let process_subdirectories f path =
+  let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in
+  process_directory f path
diff --git a/lib/system.ml b/lib/system.ml
index 8cdcaf5dc..8b53a11d6 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -12,65 +12,7 @@ open Pp
 open Errors
 open Util
 
-(** Dealing with directories *)
-
-type unix_path = string (* path in unix-style, with '/' separator *)
-
-type file_kind =
-  | FileDir of unix_path * (* basename of path: *) string
-  | FileRegular of string (* basename of file *)
-
-(* Copy of Filename.concat but assuming paths to always be POSIX *)
-
-let (//) dirname filename =
-  let l = String.length dirname in
-  if l = 0 || dirname.[l-1] = '/'
-  then dirname ^ filename
-  else dirname ^ "/" ^ filename
-
-(* Excluding directories; We avoid directories starting with . as well
-   as CVS and _darcs and any subdirs given via -exclude-dir *)
-
-let skipped_dirnames = ref ["CVS"; "_darcs"]
-
-let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames
-
-let ok_dirname f =
-  not (f = "") && f.[0] != '.' &&
-  not (List.mem f !skipped_dirnames) (*&&
-  (match Unicode.ident_refutation f with None -> true | _ -> false)*)
-
-(* Check directory can be opened *)
-
-let exists_dir dir =
-  try Sys.is_directory dir with Sys_error _ -> false
-
-let check_unix_dir warn dir =
-  if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") &&
-    (String.length dir > 2 && dir.[1] = ':' ||
-     String.contains dir '\\' ||
-     String.contains dir ';')
-  then warn ("assuming " ^ dir ^
-             " to be a Unix path even if looking like a Win32 path.")
-
-let apply_subdir f path name =
-  (* we avoid all files and subdirs starting by '.' (e.g. .svn) *)
-  (* as well as skipped files like CVS, ... *)
-  if ok_dirname name then
-    let path = if path = "." then name else path//name in
-    match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with
-    | Unix.S_DIR -> f (FileDir (path,name))
-    | Unix.S_REG -> f (FileRegular name)
-    | _ -> ()
-
-let readdir dir = try Sys.readdir dir with any -> [||]
-
-let process_directory f path =
-  Array.iter (apply_subdir f path) (readdir path)
-
-let process_subdirectories f path =
-  let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in
-  process_directory f path
+include Minisys
 
 (** Returns the list of all recursive subdirectories of [root] in
     depth-first search, with sons ordered as on the file system;
diff --git a/tools/compat5b.ml b/tools/compat5b.ml
deleted file mode 100644
index 37cb487c5..000000000
--- a/tools/compat5b.ml
+++ /dev/null
@@ -1,13 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* This file is meant for camlp5, for which there is nothing to
-   add to gain camlp5 compatibility :-).
-
-   See [compat5b.mlp] for the [camlp4] counterpart
-*)
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index c63e4aaa6..0f7937d72 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -9,11 +9,11 @@
 open Printf
 open Coqdep_lexer
 open Unix
-open System
+open Minisys
 
 (** [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.
+    are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so.
     If it need someday some additional information, pass it via
     options (see for instance [option_natdynlk] below).
 *)
@@ -526,7 +526,7 @@ let rec add_directory recur add_file phys_dir log_dir =
     | FileRegular f ->
         add_file phys_dir log_dir f
   in
-  System.check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir;
+  check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir;
   if exists_dir phys_dir then
     process_directory f phys_dir
   else