Merge PR #8763: Adapt coq_makefile to handle coqpp-based macro files.

33 files changed, 76 insertions, 51 deletions

diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml
index c2bcd73fff..d0b01453a0 100644
--- a/lib/coqProject_file.ml
+++ b/lib/coqProject_file.ml
@@ -29,6 +29,7 @@ type project = {
   v_files : string sourced list;
   mli_files : string sourced list;
   ml4_files : string sourced list;
+  mlg_files : string sourced list;
   ml_files : string sourced list;
   mllib_files : string sourced list;
   mlpack_files : string sourced list;
@@ -66,6 +67,7 @@ let mk_project project_file makefile install_kind use_ocamlopt = {
   v_files = [];
   mli_files = [];
   ml4_files = [];
+  mlg_files = [];
   ml_files = [];
   mllib_files = [];
   mlpack_files = [];
@@ -223,6 +225,7 @@ let process_cmd_line orig_dir proj args =
             { proj with v_files = proj.v_files @ [sourced f] }
         | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] }
         | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] }
+        | ".mlg" -> { proj with mlg_files = proj.mlg_files @ [sourced f] }
         | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] }
         | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] }
         | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced f] }
@@ -249,9 +252,9 @@ let rec find_project_file ~from ~projfile_name =
     else find_project_file ~from:newdir ~projfile_name
 ;;
 
-let all_files { v_files; ml_files; mli_files; ml4_files;
+let all_files { v_files; ml_files; mli_files; ml4_files; mlg_files;
                 mllib_files; mlpack_files } =
-  v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files
+  v_files @ mli_files @ ml4_files @ mlg_files @ ml_files @ mllib_files @ mlpack_files
 
 let map_sourced_list f l = List.map (fun x -> f x.thing) l
 ;;
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 5780bb5d78..2a6a09a9a0 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -23,6 +23,7 @@ type project = {
   v_files : string sourced list;
   mli_files : string sourced list;
   ml4_files : string sourced list;
+  mlg_files : string sourced list;
   ml_files : string sourced list;
   mllib_files : string sourced list;
   mlpack_files : string sourced list;
diff --git a/test-suite/coq-makefile/arg/_CoqProject b/test-suite/coq-makefile/arg/_CoqProject
index 53dc963997..ed31a58247 100644
--- a/test-suite/coq-makefile/arg/_CoqProject
+++ b/test-suite/coq-makefile/arg/_CoqProject
@@ -4,7 +4,7 @@
 -arg "-w default"
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/compat-subdirs/_CoqProject b/test-suite/coq-makefile/compat-subdirs/_CoqProject
index 4f44bde22a..1f914a71b0 100644
--- a/test-suite/coq-makefile/compat-subdirs/_CoqProject
+++ b/test-suite/coq-makefile/compat-subdirs/_CoqProject
@@ -3,7 +3,7 @@
 -I src
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/coqdoc1/_CoqProject b/test-suite/coq-makefile/coqdoc1/_CoqProject
index 35792066bb..aa9473eaf0 100644
--- a/test-suite/coq-makefile/coqdoc1/_CoqProject
+++ b/test-suite/coq-makefile/coqdoc1/_CoqProject
@@ -3,7 +3,7 @@
 -I src
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/coqdoc2/_CoqProject b/test-suite/coq-makefile/coqdoc2/_CoqProject
index d2a547d47b..0068554d72 100644
--- a/test-suite/coq-makefile/coqdoc2/_CoqProject
+++ b/test-suite/coq-makefile/coqdoc2/_CoqProject
@@ -3,7 +3,7 @@
 -I src/
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject b/test-suite/coq-makefile/emptyprefix/_CoqProject
index 5678a8edbb..3133342f6c 100644
--- a/test-suite/coq-makefile/emptyprefix/_CoqProject
+++ b/test-suite/coq-makefile/emptyprefix/_CoqProject
@@ -4,7 +4,7 @@
 -arg "-w default"
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/extend-subdirs/_CoqProject b/test-suite/coq-makefile/extend-subdirs/_CoqProject
index 69f47302e1..61136e82f0 100644
--- a/test-suite/coq-makefile/extend-subdirs/_CoqProject
+++ b/test-suite/coq-makefile/extend-subdirs/_CoqProject
@@ -3,7 +3,7 @@
 -I src
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/findlib-package/_CoqProject b/test-suite/coq-makefile/findlib-package/_CoqProject
index 69f47302e1..61136e82f0 100644
--- a/test-suite/coq-makefile/findlib-package/_CoqProject
+++ b/test-suite/coq-makefile/findlib-package/_CoqProject
@@ -3,7 +3,7 @@
 -I src
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/latex1/_CoqProject b/test-suite/coq-makefile/latex1/_CoqProject
index 35792066bb..aa9473eaf0 100644
--- a/test-suite/coq-makefile/latex1/_CoqProject
+++ b/test-suite/coq-makefile/latex1/_CoqProject
@@ -3,7 +3,7 @@
 -I src
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/merlin1/_CoqProject b/test-suite/coq-makefile/merlin1/_CoqProject
index 69f47302e1..61136e82f0 100644
--- a/test-suite/coq-makefile/merlin1/_CoqProject
+++ b/test-suite/coq-makefile/merlin1/_CoqProject
@@ -3,7 +3,7 @@
 -I src
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/mlpack1/_CoqProject b/test-suite/coq-makefile/mlpack1/_CoqProject
index 69f47302e1..61136e82f0 100644
--- a/test-suite/coq-makefile/mlpack1/_CoqProject
+++ b/test-suite/coq-makefile/mlpack1/_CoqProject
@@ -3,7 +3,7 @@
 -I src
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/mlpack2/_CoqProject b/test-suite/coq-makefile/mlpack2/_CoqProject
index 51864a87ae..3db54e0a0b 100644
--- a/test-suite/coq-makefile/mlpack2/_CoqProject
+++ b/test-suite/coq-makefile/mlpack2/_CoqProject
@@ -3,7 +3,7 @@
 -I src/
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/multiroot/_CoqProject b/test-suite/coq-makefile/multiroot/_CoqProject
index b384bb6d97..f53eef99a8 100644
--- a/test-suite/coq-makefile/multiroot/_CoqProject
+++ b/test-suite/coq-makefile/multiroot/_CoqProject
@@ -4,7 +4,7 @@
 -I src/
 
 ./src/test_plugin.mllib
-./src/test.ml4
+./src/test.mlg
 ./src/test.mli
 ./src/test_aux.ml
 ./src/test_aux.mli
diff --git a/test-suite/coq-makefile/native1/_CoqProject b/test-suite/coq-makefile/native1/_CoqProject
index a6fa17348c..847b2c00a9 100644
--- a/test-suite/coq-makefile/native1/_CoqProject
+++ b/test-suite/coq-makefile/native1/_CoqProject
@@ -4,7 +4,7 @@
 -arg -native-compiler
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/only/_CoqProject b/test-suite/coq-makefile/only/_CoqProject
index 357384fddf..619a8fa459 100644
--- a/test-suite/coq-makefile/only/_CoqProject
+++ b/test-suite/coq-makefile/only/_CoqProject
@@ -3,7 +3,7 @@
 -I src/
 
 ./src/test_plugin.mlpack
-./src/test.ml4
+./src/test.mlg
 ./src/test.mli
 ./src/test_aux.ml
 ./src/test_aux.mli
diff --git a/test-suite/coq-makefile/plugin1/_CoqProject b/test-suite/coq-makefile/plugin1/_CoqProject
index 4eddc9d708..ab7876d868 100644
--- a/test-suite/coq-makefile/plugin1/_CoqProject
+++ b/test-suite/coq-makefile/plugin1/_CoqProject
@@ -3,7 +3,7 @@
 -I src
 
 src/test_plugin.mllib
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/plugin2/_CoqProject b/test-suite/coq-makefile/plugin2/_CoqProject
index 0bf1e07f25..94eed53130 100644
--- a/test-suite/coq-makefile/plugin2/_CoqProject
+++ b/test-suite/coq-makefile/plugin2/_CoqProject
@@ -3,7 +3,7 @@
 -I src/
 
 src/test_plugin.mllib
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/plugin3/_CoqProject b/test-suite/coq-makefile/plugin3/_CoqProject
index 2028d49a8b..8e8a7ab074 100644
--- a/test-suite/coq-makefile/plugin3/_CoqProject
+++ b/test-suite/coq-makefile/plugin3/_CoqProject
@@ -3,7 +3,7 @@
 -I src/
 
 ./src/test_plugin.mllib
-./src/test.ml4
+./src/test.mlg
 ./src/test.mli
 ./src/test_aux.ml
 ./src/test_aux.mli
diff --git a/test-suite/coq-makefile/quick2vo/_CoqProject b/test-suite/coq-makefile/quick2vo/_CoqProject
index 69f47302e1..61136e82f0 100644
--- a/test-suite/coq-makefile/quick2vo/_CoqProject
+++ b/test-suite/coq-makefile/quick2vo/_CoqProject
@@ -3,7 +3,7 @@
 -I src
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh
index 2e066d30d9..30be5e6456 100755
--- a/test-suite/coq-makefile/template/init.sh
+++ b/test-suite/coq-makefile/template/init.sh
@@ -11,7 +11,7 @@ mkdir -p theories/sub
 
 cp ../../template/theories/sub/testsub.v theories/sub
 cp ../../template/theories/test.v theories
-cp ../../template/src/test.ml4 src
+cp ../../template/src/test.mlg src
 cp ../../template/src/test_aux.mli src
 cp ../../template/src/test.mli src
 cp ../../template/src/test_plugin.mlpack src
diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.mlg
index 72765abe04..7a166f3b98 100644
--- a/test-suite/coq-makefile/template/src/test.ml4
+++ b/test-suite/coq-makefile/template/src/test.mlg
@@ -1,13 +1,17 @@
+{
 open Ltac_plugin
+}
 DECLARE PLUGIN "test_plugin"
+{
 let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
+}
 
 VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
-  | [ "TestCommand" ] -> [ () ]
+  | [ "TestCommand" ] -> { () }
 END
 
 TACTIC EXTEND test
-| [ "test_tactic" ] -> [ Test_aux.tac ]
+| [ "test_tactic" ] -> { Test_aux.tac }
 END
 
 
diff --git a/test-suite/coq-makefile/uninstall1/_CoqProject b/test-suite/coq-makefile/uninstall1/_CoqProject
index 35792066bb..aa9473eaf0 100644
--- a/test-suite/coq-makefile/uninstall1/_CoqProject
+++ b/test-suite/coq-makefile/uninstall1/_CoqProject
@@ -3,7 +3,7 @@
 -I src
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/uninstall2/_CoqProject b/test-suite/coq-makefile/uninstall2/_CoqProject
index d2a547d47b..0068554d72 100644
--- a/test-suite/coq-makefile/uninstall2/_CoqProject
+++ b/test-suite/coq-makefile/uninstall2/_CoqProject
@@ -3,7 +3,7 @@
 -I src/
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/validate1/_CoqProject b/test-suite/coq-makefile/validate1/_CoqProject
index 69f47302e1..61136e82f0 100644
--- a/test-suite/coq-makefile/validate1/_CoqProject
+++ b/test-suite/coq-makefile/validate1/_CoqProject
@@ -3,7 +3,7 @@
 -I src
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/coq-makefile/vio2vo/_CoqProject b/test-suite/coq-makefile/vio2vo/_CoqProject
index 69f47302e1..61136e82f0 100644
--- a/test-suite/coq-makefile/vio2vo/_CoqProject
+++ b/test-suite/coq-makefile/vio2vo/_CoqProject
@@ -3,7 +3,7 @@
 -I src
 
 src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
 src/test.mli
 src/test_aux.ml
 src/test_aux.mli
diff --git a/test-suite/misc/poly-capture-global-univs/_CoqProject b/test-suite/misc/poly-capture-global-univs/_CoqProject
index 70ec246062..e5dc3cff56 100644
--- a/test-suite/misc/poly-capture-global-univs/_CoqProject
+++ b/test-suite/misc/poly-capture-global-univs/_CoqProject
@@ -1,7 +1,7 @@
 -Q theories Evil
 -I src
 
-src/evil.ml4
+src/evil.mlg
 src/evilImpl.ml
 src/evilImpl.mli
 src/evil_plugin.mlpack
diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.ml4 b/test-suite/misc/poly-capture-global-univs/src/evil.ml4
deleted file mode 100644
index 565e979aaa..0000000000
--- a/test-suite/misc/poly-capture-global-univs/src/evil.ml4
+++ /dev/null
@@ -1,9 +0,0 @@
-
-open Stdarg
-open EvilImpl
-
-DECLARE PLUGIN "evil_plugin"
-
-VERNAC COMMAND FUNCTIONAL EXTEND VernacEvil CLASSIFIED AS SIDEFF
-| [ "Evil" ident(x) ident(y) ] -> [ fun ~atts ~st -> evil x y; st ]
-END
diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.mlg b/test-suite/misc/poly-capture-global-univs/src/evil.mlg
new file mode 100644
index 0000000000..edd22b1d29
--- /dev/null
+++ b/test-suite/misc/poly-capture-global-univs/src/evil.mlg
@@ -0,0 +1,10 @@
+{
+open Stdarg
+open EvilImpl
+}
+
+DECLARE PLUGIN "evil_plugin"
+
+VERNAC COMMAND EXTEND VernacEvil CLASSIFIED AS SIDEFF
+| [ "Evil" ident(x) ident(y) ] -> { evil x y }
+END
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 403ad61798..e3fa0c24fe 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -21,6 +21,7 @@ VFILES            := $(COQMF_VFILES)
 MLIFILES          := $(COQMF_MLIFILES)
 MLFILES           := $(COQMF_MLFILES)
 ML4FILES          := $(COQMF_ML4FILES)
+MLGFILES          := $(COQMF_MLGFILES)
 MLPACKFILES       := $(COQMF_MLPACKFILES)
 MLLIBFILES        := $(COQMF_MLLIBFILES)
 CMDLINE_VFILES    := $(COQMF_CMDLINE_VFILES)
@@ -87,6 +88,7 @@ COQTOP   ?= "$(COQBIN)coqtop"
 COQCHK   ?= "$(COQBIN)coqchk"
 COQDEP   ?= "$(COQBIN)coqdep"
 COQDOC   ?= "$(COQBIN)coqdoc"
+COQPP    ?= "$(COQBIN)coqpp"
 COQMKFILE ?= "$(COQBIN)coq_makefile"
 
 # Timing scripts
@@ -241,6 +243,7 @@ VDFILE := .coqdeps
 
 ALLSRCFILES := \
 	$(ML4FILES) \
+	$(MLGFILES) \
 	$(MLFILES) \
 	$(MLPACKFILES) \
 	$(MLLIBFILES) \
@@ -262,6 +265,7 @@ TEXFILES = $(VFILES:.v=.tex)
 GTEXFILES = $(VFILES:.v=.g.tex)
 CMOFILES = \
 	$(ML4FILES:.ml4=.cmo) \
+	$(MLGFILES:.mlg=.cmo) \
 	$(MLFILES:.ml=.cmo) \
 	$(MLPACKFILES:.mlpack=.cmo)
 CMXFILES = $(CMOFILES:.cmo=.cmx)
@@ -277,7 +281,7 @@ CMXSFILES = \
 	$(MLPACKFILES:.mlpack=.cmxs) \
 	$(CMXAFILES:.cmxa=.cmxs) \
 	$(if $(MLPACKFILES)$(CMXAFILES),,\
-		$(ML4FILES:.ml4=.cmxs) $(MLFILES:.ml=.cmxs))
+		$(ML4FILES:.ml4=.cmxs) $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs))
 
 # files that are packed into a plugin (no extension)
 PACKEDFILES = \
@@ -555,6 +559,7 @@ clean::
 	$(HIDE)rm -f $(CMXSFILES)
 	$(HIDE)rm -f $(CMOFILES:.cmo=.o)
 	$(HIDE)rm -f $(CMXAFILES:.cmxa=.a)
+	$(HIDE)rm -f $(MLGFILES:.mlg=.ml)
 	$(HIDE)rm -f $(ALLDFILES)
 	$(HIDE)rm -f $(NATIVEFILES)
 	$(HIDE)find . -name .coq-native -type d -empty -delete
@@ -602,11 +607,17 @@ $(ML4FILES:.ml4=.cmx): %.cmx: %.ml4
 	$(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<'
 	$(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $<
 
-$(MLFILES:.ml=.cmo): %.cmo: %.ml
+$(MLGFILES:.mlg=.ml): %.ml: %.mlg
+	$(SHOW)'COQPP $<'
+	$(HIDE)$(COQPP) $<
+
+# Stupid hack around a deficient syntax: we cannot concatenate two expansions
+$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml
 	$(SHOW)'CAMLC -c $<'
 	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
 
-$(MLFILES:.ml=.cmx): %.cmx: %.ml
+# Same hack
+$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml
 	$(SHOW)'CAMLOPT -c $(FOR_PACK) $<'
 	$(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $<
 
@@ -647,7 +658,7 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
 	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
 
 # This rule is for _CoqProject with no .mllib nor .mlpack
-$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx
+$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx
 	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
 	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
 		-shared -o $@ $<
@@ -716,6 +727,10 @@ $(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4
 	$(SHOW)'CAMLDEP -pp $<'
 	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok)
 
+$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
+
 $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml
 	$(SHOW)'CAMLDEP $<'
 	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 7bb1390cad..ca5a232edb 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -218,7 +218,7 @@ let generate_conf_coq_config oc =
 ;;
 
 let generate_conf_files oc
-  { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files; }
+  { v_files; mli_files; ml4_files; mlg_files; ml_files; mllib_files; mlpack_files; }
 =
   let module S = String in
   let map = map_sourced_list in
@@ -227,6 +227,7 @@ let generate_conf_files oc
   fprintf oc "COQMF_MLIFILES = %s\n"    (S.concat " " (map quote mli_files));
   fprintf oc "COQMF_MLFILES = %s\n"     (S.concat " " (map quote ml_files));
   fprintf oc "COQMF_ML4FILES = %s\n"    (S.concat " " (map quote ml4_files));
+  fprintf oc "COQMF_MLGFILES = %s\n"    (S.concat " " (map quote mlg_files));
   fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files));
   fprintf oc "COQMF_MLLIBFILES = %s\n"  (S.concat " " (map quote mllib_files));
   let cmdline_vfiles = filter_cmdline v_files in
@@ -283,7 +284,7 @@ let generate_conf oc project args  =
 
 let ensure_root_dir
   ({ ml_includes; r_includes; q_includes;
-     v_files; ml_files; mli_files; ml4_files;
+     v_files; ml_files; mli_files; ml4_files; mlg_files;
      mllib_files; mlpack_files } as project)
   =
   let exists f = List.exists (forget_source > f) in
@@ -293,8 +294,8 @@ let ensure_root_dir
   || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes
   || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes
   || (not_tops v_files &&
-      not_tops mli_files && not_tops ml4_files && not_tops ml_files &&
-      not_tops mllib_files && not_tops mlpack_files)
+      not_tops mli_files && not_tops ml4_files && not_tops mlg_files &&
+      not_tops ml_files && not_tops mllib_files && not_tops mlpack_files)
   then
     project
   else
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 6a913ea894..713b2ad2b6 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -496,9 +496,9 @@ let rec suffixes = function
 
 let add_caml_known phys_dir _ f =
   let basename,suff =
-    get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] in
+    get_extension f [".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] in
   match suff with
-    | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff
+    | ".ml"|".ml4"|".mlg" -> add_ml_known basename (Some phys_dir) suff
     | ".mli" -> add_mli_known basename (Some phys_dir) suff
     | ".mllib" -> add_mllib_known basename (Some phys_dir) suff
     | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff
@@ -584,12 +584,12 @@ let rec treat_file old_dirname old_name =
 	   in
            Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name))
     | S_REG ->
-	(match get_extension name [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with
+        (match get_extension name [".v";".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] with
 	   | (base,".v") ->
 	       let name = file_name base dirname
 	       and absname = absolute_file_name base dirname in
 	       addQueue vAccu (name, absname)
-	   | (base,(".ml"|".ml4" as ext)) -> addQueue mlAccu (base,ext,dirname)
+           | (base,(".ml"|".ml4"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname)
 	   | (base,".mli") -> addQueue mliAccu (base,dirname)
 	   | (base,".mllib") -> addQueue mllibAccu (base,dirname)
 	   | (base,".mlpack") -> addQueue mlpackAccu (base,dirname)
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
index 053a0435ce..155296362f 100644
--- a/tools/ocamllibdep.mll
+++ b/tools/ocamllibdep.mll
@@ -145,9 +145,9 @@ let mllibAccu = ref ([] : (string * dir) list)
 let mlpackAccu = ref ([] : (string * dir) list)
 
 let add_caml_known phys_dir f =
-  let basename,suff = get_extension f [".ml";".ml4";".mlpack"] in
+  let basename,suff = get_extension f [".ml";".ml4";".mlg";".mlpack"] in
   match suff with
-    | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff
+    | ".ml"|".ml4"|".mlg" -> add_ml_known basename (Some phys_dir) suff
     | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff
     | _ -> ()