Remove ml4 from Coq's make build system

3 files changed, 17 insertions, 27 deletions

diff --git a/Makefile b/Makefile
index b9d8bf34e3..e0ab169eda 100644
--- a/Makefile
+++ b/Makefile
@@ -78,7 +78,6 @@ LEXFILES := $(call find, '*.mll')
 YACCFILES := $(call find, '*.mly')
 export MLLIBFILES := $(call find, '*.mllib')
 export MLPACKFILES := $(call find, '*.mlpack')
-export ML4FILES := $(call find, '*.ml4')
 export MLGFILES := $(call find, '*.mlg')
 export CFILES := $(call findindir, 'kernel/byterun', '*.c')
 
@@ -94,19 +93,14 @@ EXISTINGMLI := $(call find, '*.mli')
 
 ## Files that will be generated
 
-GENML4FILES:= $(ML4FILES:.ml4=.ml)
 GENMLGFILES:= $(MLGFILES:.mlg=.ml)
-export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml
+export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES)  ide/coqide_os_specific.ml kernel/copcodes.ml
 export GENHFILES:=kernel/byterun/coq_jumptbl.h
 export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
 
-# NB: all files in $(GENFILES) can be created initially, while
-# .ml files in $(GENML4FILES) might need some intermediate building.
-# That's why we keep $(GENML4FILES) out of $(GENFILES)
-
 ## More complex file lists
 
-export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES) $(GENMLGFILES), $(EXISTINGML))
+export MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML))
 export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
 
 include Makefile.common
@@ -194,7 +188,7 @@ META.coq: META.coq.in
 # Cleaning
 ###########################################################################
 
-.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean alienclean
+.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean
 
 clean: objclean cruftclean depclean docclean camldevfilesclean
 
@@ -202,7 +196,7 @@ cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean
 
 objclean: archclean indepclean
 
-cruftclean: ml4clean
+cruftclean: mlgclean
 	find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} +
 	rm -f gmon.out core
 
@@ -252,8 +246,8 @@ clean-ide:
 	rm -f ide/utf8_convert.ml
 	rm -rf $(COQIDEAPP)
 
-ml4clean:
-	rm -f $(GENML4FILES) $(GENMLGFILES)
+mlgclean:
+	rm -f $(GENMLGFILES)
 
 depclean:
 	find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} +
@@ -286,7 +280,7 @@ KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v'))
 ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO))
 
 EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa')
-KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \
+KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(MLPACKFILES:.mlpack=.ml) \
  $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp))
 KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \
  $(MLIFILES:.mli=.cmi) \
@@ -308,7 +302,7 @@ include Makefile.ci
 .PHONY: tags printenv
 
 tags:
-	echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \
+	echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \
 	etags --language=none\
 	      "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
@@ -317,12 +311,12 @@ tags:
               "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"
-	echo $(ML4FILES) | sort -r | xargs \
+	echo $(MLGFILES) | sort -r | xargs \
 	etags --append --language=none\
 	      "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/"
 
 checker-tags:
-	echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \
+	echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \
 	etags --language=none\
 	      "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
@@ -331,7 +325,7 @@ checker-tags:
               "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"
-	echo $(ML4FILES) | sort -r | xargs \
+	echo $(MLGFILES) | sort -r | xargs \
 	etags --append --language=none\
 	      "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/"
 
diff --git a/Makefile.build b/Makefile.build
index 08863014ea..fb84a131c7 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -86,7 +86,7 @@ byte: coqbyte coqide-byte pluginsbyte printers
 
 # This list of ml files used to be in the main Makefile, we moved it here
 # to avoid exhausting the variable env in Win32
-MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
+MLFILES := $(MLSTATICFILES) $(GENMLFILES)
 
 include Makefile.common
 include Makefile.vofiles
@@ -148,7 +148,7 @@ endif
 # This include below will lauch the build of all .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).
+# coqdep_boot (for the .v.d files) or coqpp (for .mlg -> .ml -> .ml.d).
 
 VDFILE := .vfiles
 MLDFILE := .mlfiles
@@ -166,7 +166,7 @@ DEPENDENCIES := \
 # of include, and they will then be automatically deleted, leading to an
 # infinite loop.
 
-.SECONDARY: $(DEPENDENCIES) $(GENFILES) $(ML4FILES:.ml4=.ml)
+.SECONDARY: $(DEPENDENCIES) $(GENFILES) $(MLGFILES:.mlg=.ml)
 
 ###########################################################################
 # Compilation options
@@ -259,6 +259,7 @@ CAMLP5DEPS:=grammar/grammar.cma
 CAMLP5USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
 
 PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo)
+# XXX unused but should be used for mlp files
 
 # Main packages linked by Coq.
 SYSMOD:=-package num,str,unix,dynlink,threads
@@ -768,11 +769,6 @@ kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50
 	$(SHOW)'OCAMLYACC  $<'
 	$(HIDE)$(OCAMLYACC) --strict "$*.mly"
 
-%.ml: %.ml4 $(CAMLP5DEPS) $(COQPP)
-	$(SHOW)'CAMLP5O   $<'
-	$(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) \
-	  $(CAMLP5DEPS) $(CAMLP5USE) $(CAMLP5COMPAT) -impl $< -o $@
-
 %.ml: %.mlg $(COQPP)
 	$(SHOW)'COQPP   $<'
 	$(HIDE)$(COQPP) $<
@@ -782,7 +778,7 @@ kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50
 ###########################################################################
 
 # Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12)
-OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
+OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .mlpack
 
 MAINMLFILES := $(filter-out checker/% plugins/%, $(MLFILES) $(MLIFILES))
 MAINMLLIBFILES := $(filter-out checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES))
diff --git a/dev/tools/change-header b/dev/tools/change-header
index 61cc866602..687c02f4f1 100755
--- a/dev/tools/change-header
+++ b/dev/tools/change-header
@@ -22,7 +22,7 @@ lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)'
 modified=0
 kept=0
 
-for i in `find . -name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do
+for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do
   headline=`head -n 1 $i`
   if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then
       # Has emacs header