diff options
| -rw-r--r-- | doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst | 6 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 10 |
2 files changed, 16 insertions, 0 deletions
diff --git a/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst b/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst new file mode 100644 index 0000000000..a43e950bff --- /dev/null +++ b/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst @@ -0,0 +1,6 @@ +- **Deprecated:** + The `-load-ml-source` and `-load-ml-object` command line options + have been deprecated; their use was very limited, you can achieve the same adding + additional object files in the linking step or by using a plugin. + (`#11428 <https://github.com/coq/coq/pull/11428>`_, + by Emilio Jesus Gallego Arias). diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 5326ce6114..56a6312b61 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -198,6 +198,14 @@ let set_query opts q = | Queries queries -> Queries (queries@[q]) } +let warn_depr_load_ml_object = + CWarnings.create ~name:"deprecated-mlobject" ~category:"deprecated" + (fun () -> Pp.strbrk "The -load-ml-object option is deprecated, see the changelog for more details.") + +let warn_depr_ml_load_source = + CWarnings.create ~name:"deprecated-mlsource" ~category:"deprecated" + (fun () -> Pp.strbrk "The -load-ml-source option is deprecated, see the changelog for more details.") + let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") @@ -396,9 +404,11 @@ let parse_args ~help ~init arglist : t * string list = set_inputstate oval (next ()) |"-load-ml-object" -> + warn_depr_load_ml_object (); Mltop.dir_ml_load (next ()); oval |"-load-ml-source" -> + warn_depr_ml_load_source (); Mltop.dir_ml_use (next ()); oval |"-load-vernac-object" -> |