diff options
| author | Emilio Jesus Gallego Arias | 2018-12-04 17:18:40 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-04 17:18:40 +0100 |
| commit | 12e99660de15f6f6c6d78344cf48b16f46032f0a (patch) | |
| tree | 64ed51d01ca9cef30dcfcbe61626c687bc93f4ea /lib | |
| parent | a7f13c1c3b8ff86ec68a107937e720b80e09d520 (diff) | |
| parent | 54b96940073aa1506dd6d4ed0fe8277c6360ef54 (diff) | |
Merge PR #9127: Remove leftover code that used to handle ml4 files.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coqProject_file.ml | 10 | ||||
| -rw-r--r-- | lib/coqProject_file.mli | 1 |
2 files changed, 5 insertions, 6 deletions
diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml index 868042303d..d908baa1e8 100644 --- a/lib/coqProject_file.ml +++ b/lib/coqProject_file.ml @@ -24,7 +24,6 @@ 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; @@ -62,7 +61,6 @@ let mk_project project_file makefile install_kind use_ocamlopt = { v_files = []; mli_files = []; - ml4_files = []; mlg_files = []; ml_files = []; mllib_files = []; @@ -220,7 +218,9 @@ let process_cmd_line ~warning_fn orig_dir proj args = | ".v" -> { 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] } + | ".ml4" -> + let msg = Printf.sprintf "camlp5 macro files not supported anymore, please port %s to coqpp" f in + raise (Parsing_error msg) | ".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] } @@ -248,9 +248,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; mlg_files; +let all_files { v_files; ml_files; mli_files; mlg_files; mllib_files; mlpack_files } = - 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 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 20b276ce8c..39c5d019d0 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -22,7 +22,6 @@ 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; |