diff options
| -rw-r--r-- | CHANGES.md | 8 | ||||
| -rw-r--r-- | plugins/quote/plugin_base.dune | 5 | ||||
| -rw-r--r-- | plugins/setoid_ring/plugin_base.dune | 2 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 3 | ||||
| -rw-r--r-- | tools/dune | 22 |
5 files changed, 22 insertions, 18 deletions
diff --git a/CHANGES.md b/CHANGES.md index 302e952cf6..865e1eeb95 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -42,6 +42,14 @@ Notations `Bind Scope`, `Delimit Scope`, `Undelimit Scope`, or `Notation` is deprecated. +- Deprecated compatibility notations will actually be removed in the + next version of Coq. Uses of these notations are generally easy to + fix thanks to the hint contained in the deprecation warnings. For + projects that require more than a handful of such fixes, there is [a + script](https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py) + that will do it automatically, using the output of coqc. The script + contains documentation on its usage in a comment at the top. + Tactics - Added toplevel goal selector `!` which expects a single focused goal. diff --git a/plugins/quote/plugin_base.dune b/plugins/quote/plugin_base.dune deleted file mode 100644 index 323906acb2..0000000000 --- a/plugins/quote/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name quote_plugin) - (public_name coq.plugins.quote) - (synopsis "Coq's quote plugin") - (libraries coq.plugins.ltac)) diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/plugin_base.dune index 101246e28f..d83857edad 100644 --- a/plugins/setoid_ring/plugin_base.dune +++ b/plugins/setoid_ring/plugin_base.dune @@ -2,4 +2,4 @@ (name newring_plugin) (public_name coq.plugins.setoid_ring) (synopsis "Coq's setoid ring plugin") - (libraries coq.plugins.quote)) + (libraries coq.plugins.ltac)) diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index ff6cefdf24..4f4e6d5d6f 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -226,7 +226,8 @@ let scan_mlg4 m d = List.fold_left (fun m f -> add_map_list ["plugins"; d] (choose_ml4g_form f) m) m ml4 let scan_plugins m = - let dirs = Sys.(List.filter (fun f -> is_directory @@ "plugins/"^f) Array.(to_list @@ readdir "plugins/")) in + let is_plugin_directory dir = Sys.(is_directory dir && file_exists (dir ^ "/plugin_base.dune")) in + let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ "plugins/"^f) Array.(to_list @@ readdir "plugins/")) in List.fold_left scan_mlg4 m dirs (* Process .vfiles.d and generate a skeleton for the dune file *) diff --git a/tools/dune b/tools/dune index 3358d1a4e2..31b70fb06c 100644 --- a/tools/dune +++ b/tools/dune @@ -23,6 +23,13 @@ (libraries coq.toplevel)) (executable + (name coqworkmgr) + (public_name coqworkmgr) + (package coq) + (modules coqworkmgr) + (libraries coq.stm)) + +(executable (name coqdep) (public_name coqdep) (package coq) @@ -40,16 +47,9 @@ (ocamllex coqwc) -(executable - (name coq_tex) - (public_name coq_tex) - (package coq) - (modules coq_tex) - (libraries str)) - -(executable - (name coq_dune) - (public_name coq_dune) +(executables + (names coq_tex coq_dune) + (public_names coq-tex coq_dune) (package coq) - (modules coq_dune) + (modules coq_tex coq_dune) (libraries str)) |