Remove leftover code that used to handle ml4 files.

5 files changed, 21 insertions, 46 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index b673225e40..4372ac72ae 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -102,7 +102,7 @@ CAMLOPTC    ?= "$(OCAMLFIND)" opt      -c
 CAMLLINK    ?= "$(OCAMLFIND)" ocamlc   -linkpkg -dontlink $(CAMLDONTLINK)
 CAMLOPTLINK ?= "$(OCAMLFIND)" opt      -linkpkg -dontlink $(CAMLDONTLINK)
 CAMLDOC     ?= "$(OCAMLFIND)" ocamldoc
-CAMLDEP     ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
+CAMLDEP     ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack
 
 # DESTDIR is prepended to all installation paths
 DESTDIR ?=
@@ -226,7 +226,6 @@ COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop)
 VDFILE := .coqdeps
 
 ALLSRCFILES := \
-	$(ML4FILES) \
 	$(MLGFILES) \
 	$(MLFILES) \
 	$(MLPACKFILES) \
@@ -248,7 +247,6 @@ BEAUTYFILES = $(addsuffix .beautified,$(VFILES))
 TEXFILES = $(VFILES:.v=.tex)
 GTEXFILES = $(VFILES:.v=.g.tex)
 CMOFILES = \
-	$(ML4FILES:.ml4=.cmo) \
 	$(MLGFILES:.mlg=.cmo) \
 	$(MLFILES:.ml=.cmo) \
 	$(MLPACKFILES:.mlpack=.cmo)
@@ -265,7 +263,7 @@ CMXSFILES = \
 	$(MLPACKFILES:.mlpack=.cmxs) \
 	$(CMXAFILES:.cmxa=.cmxs) \
 	$(if $(MLPACKFILES)$(CMXAFILES),,\
-		$(ML4FILES:.ml4=.cmxs) $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs))
+		$(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs))
 
 # files that are packed into a plugin (no extension)
 PACKEDFILES = \
@@ -583,14 +581,6 @@ $(MLIFILES:.mli=.cmi): %.cmi: %.mli
 	$(SHOW)'CAMLC -c $<'
 	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
 
-$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4
-	$(SHOW)'CAMLC -pp -c $<'
-	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) -impl $<
-
-$(ML4FILES:.ml4=.cmx): %.cmx: %.ml4
-	$(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<'
-	$(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $<
-
 $(MLGFILES:.mlg=.ml): %.ml: %.mlg
 	$(SHOW)'COQPP $<'
 	$(HIDE)$(COQPP) $<
@@ -642,7 +632,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) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx
+$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx
 	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
 	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
 		-shared -o $@ $<
@@ -703,17 +693,13 @@ endif
 
 redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV )
 
-GENMLFILES:=$(MLGFILES:.mlg=.ml) $(ML4FILES:.ml4=.ml)
+GENMLFILES:=$(MLGFILES:.mlg=.ml)
 $(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES)
 
 $(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli
 	$(SHOW)'CAMLDEP $<'
 	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
 
-$(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)
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index 84850e7158..41057a79e0 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -136,7 +136,7 @@ type vodep = {
   deps : string list;
 }
 
-type ldep = | VO of vodep | ML4 of string | MLG of string
+type ldep = | VO of vodep | MLG of string
 type ddir = ldep list DirMap.t
 
 (* Filter `.vio` etc... *)
@@ -181,19 +181,13 @@ let pp_vo_dep dir fmt vo =
   let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s %s -compile %s))" libflag eflag cflag source in
   pp_rule fmt [vo.target] deps action
 
-let pp_ml4_dep _dir fmt ml =
-  let target = Filename.(remove_extension ml) ^ ".ml" in
-  let ml4_rule = "(run coqp5 -loc loc -impl %{pp-file} -o %{targets})" in
-  pp_rule fmt [target] [ml] ml4_rule
-
 let pp_mlg_dep _dir fmt ml =
   let target = Filename.(remove_extension ml) ^ ".ml" in
-  let ml4_rule = "(run coqpp %{pp-file})" in
-  pp_rule fmt [target] [ml] ml4_rule
+  let mlg_rule = "(run coqpp %{pp-file})" in
+  pp_rule fmt [target] [ml] mlg_rule
 
 let pp_dep dir fmt oo = match oo with
   | VO vo -> pp_vo_dep dir fmt vo
-  | ML4 f -> pp_ml4_dep dir fmt f
   | MLG f -> pp_mlg_dep dir fmt f
 
 let out_install fmt dir ff =
@@ -220,21 +214,17 @@ let record_dune d ff =
     eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd
 
 (* File Scanning *)
-let choose_ml4g_form f =
-  if Filename.check_suffix f ".ml4" then ML4 f
-  else MLG f
-
-let scan_mlg4 m d =
+let scan_mlg m d =
   let dir = ["plugins"; d] in
   let m = DirMap.add dir [] m in
-  let ml4 = Sys.(List.filter (fun f -> Filename.(check_suffix f ".ml4" || check_suffix f ".mlg"))
+  let mlg = Sys.(List.filter (fun f -> Filename.(check_suffix f ".mlg"))
                    Array.(to_list @@ readdir (bpath dir))) in
-  List.fold_left (fun m f -> add_map_list ["plugins"; d] (choose_ml4g_form f) m) m ml4
+  List.fold_left (fun m f -> add_map_list ["plugins"; d] (MLG f) m) m mlg
 
 let scan_plugins m =
   let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in
   let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath ["plugins";f]) Array.(to_list @@ readdir "plugins")) in
-  List.fold_left scan_mlg4 m dirs
+  List.fold_left scan_mlg m dirs
 
 (* Process .vfiles.d and generate a skeleton for the dune file *)
 let parse_coqdep_line l =
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 8560bac786..5fd894e908 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; mlg_files; ml_files; mllib_files; mlpack_files; }
+  { v_files; mli_files; mlg_files; ml_files; mllib_files; mlpack_files; }
 =
   let module S = String in
   let map = map_sourced_list in
@@ -226,7 +226,6 @@ let generate_conf_files oc
   fprintf oc "COQMF_VFILES = %s\n"      (S.concat " " (map quote v_files));
   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));
@@ -284,7 +283,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; mlg_files;
+     v_files; ml_files; mli_files; mlg_files;
      mllib_files; mlpack_files } as project)
   =
   let exists f = List.exists (forget_source > f) in
@@ -294,7 +293,7 @@ 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 mlg_files &&
+      not_tops mli_files && not_tops mlg_files &&
       not_tops ml_files && not_tops mllib_files && not_tops mlpack_files)
   then
     project
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 713b2ad2b6..db2031c64b 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -62,7 +62,7 @@ let basename_noext filename =
 (** ML Files specified on the command line. In the entries:
     - the first string is the basename of the file, without extension nor
       directory part
-    - the second string of [mlAccu] is the extension (either .ml or .ml4)
+    - the second string of [mlAccu] is the extension (either .ml or .mlg)
     - the [dir] part is the directory, with None used as the current directory
 *)
 
@@ -496,9 +496,9 @@ let rec suffixes = function
 
 let add_caml_known phys_dir _ f =
   let basename,suff =
-    get_extension f [".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] in
+    get_extension f [".ml";".mli";".mlg";".mllib";".mlpack"] in
   match suff with
-    | ".ml"|".ml4"|".mlg" -> add_ml_known basename (Some phys_dir) suff
+    | ".ml"|".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";".mlg";".mllib";".mlpack"] with
+        (match get_extension name [".v";".ml";".mli";".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"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname)
+           | (base,(".ml"|".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 155296362f..680c8f30ae 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";".mlg";".mlpack"] in
+  let basename,suff = get_extension f [".ml";".mlg";".mlpack"] in
   match suff with
-    | ".ml"|".ml4"|".mlg" -> add_ml_known basename (Some phys_dir) suff
+    | ".ml"|".mlg" -> add_ml_known basename (Some phys_dir) suff
     | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff
     | _ -> ()