diff options
| -rw-r--r-- | doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 2 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.ml | 2 | ||||
| -rw-r--r-- | topbin/coqtop_byte_bin.ml | 1 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 16 | ||||
| -rw-r--r-- | toplevel/usage.ml | 2 | ||||
| -rw-r--r-- | vernac/mltop.ml | 13 | ||||
| -rw-r--r-- | vernac/mltop.mli | 7 |
8 files changed, 6 insertions, 42 deletions
diff --git a/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst b/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst new file mode 100644 index 0000000000..db433ad64c --- /dev/null +++ b/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst @@ -0,0 +1,5 @@ +- **Removed:** + The `-load-ml-source` and `-load-ml-object` command line options + have been removed; their use was very limited, you can achieve the same adding + additional object files in the linking step or using a plugin. + (`#11409 <https://github.com/coq/coq/pull/11409>`_, by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index ba43128bdc..98d222e317 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -157,8 +157,6 @@ and ``coqtop``, unless stated otherwise: loading the default resource file from the standard configuration directories. :-q: Do not to load the default resource file. -:-load-ml-source *file*: Load the OCaml source file *file*. -:-load-ml-object *file*: Load the OCaml object file *file*. :-l *file*, -load-vernac-source *file*: Load and execute the |Coq| script from *file.v*. :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 909804d0c9..fd689602df 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -138,7 +138,7 @@ module Make(T : Task) () = struct set_slave_opt tl (* We need to pass some options with one argument *) | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat" - | "-load-ml-object" | "-load-ml-source" | "-require" | "-w" | "-color" | "-init-file" + | "-require" | "-w" | "-color" | "-init-file" | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" | "-set" | "-unset" | "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl -> x :: a :: set_slave_opt tl diff --git a/topbin/coqtop_byte_bin.ml b/topbin/coqtop_byte_bin.ml index 85d8a48eda..604c6e251a 100644 --- a/topbin/coqtop_byte_bin.ml +++ b/topbin/coqtop_byte_bin.ml @@ -31,7 +31,6 @@ let drop_setup () = { load_obj = (fun f -> if not (Topdirs.load_file ppf f) then CErrors.user_err Pp.(str ("Could not load plugin "^f)) ); - use_file = Topdirs.dir_use ppf; add_dir = Topdirs.dir_directory; ml_loop = (fun () -> Toploop.loop ppf); }) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 52e2562ae8..74d9c113d6 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -198,14 +198,6 @@ 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.") @@ -403,14 +395,6 @@ let parse_args ~help ~init arglist : t * string list = |"-inputstate"|"-is" -> 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" -> add_vo_require oval (next ()) None None diff --git a/toplevel/usage.ml b/toplevel/usage.ml index b17ca71f4c..051638d53c 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -36,8 +36,6 @@ let print_usage_common co command = \n -nois (idem)\ \n -compat X.Y provides compatibility support for Coq version X.Y\ \n\ -\n -load-ml-object f load ML object file f\ -\n -load-ml-source f load ML file f\ \n -load-vernac-source f load Coq file f.v (Load \"f\".)\ \n -l f (idem)\ \n -load-vernac-source-verbose f load Coq file f.v (Load Verbose \"f\".)\ diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 6621c1e6b1..2bac35b08f 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -56,7 +56,6 @@ let keep_copy_mlpath path = (* If there is a toplevel under Coq *) type toplevel = { load_obj : string -> unit; - use_file : string -> unit; add_dir : string -> unit; ml_loop : unit -> unit } @@ -123,17 +122,6 @@ let dir_ml_load s = let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in ml_load gname -(* Dynamic interpretation of .ml *) -let dir_ml_use s = - match !load with - | WithTop t -> t.use_file s - | _ -> - let moreinfo = - if Sys.(backend_type = Native) then " Loading ML code works only in bytecode." - else "" - in - user_err ~hdr:"Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo) - (* Adds a path to the ML paths *) let add_ml_dir s = match !load with @@ -258,7 +246,6 @@ let load_ml_object mname ?path fname= init_ml_object mname; path -let dir_ml_load m = ignore(dir_ml_load m) let add_known_module m = add_known_module m None (* Summary of declared ML Modules *) diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 56a28b64b0..271772d7ba 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -14,7 +14,6 @@ record. *) type toplevel = { load_obj : string -> unit; - use_file : string -> unit; add_dir : string -> unit; ml_loop : unit -> unit } @@ -38,12 +37,6 @@ val add_ml_dir : recursive:bool -> string -> unit (** Tests if we can load ML files *) val has_dynlink : bool -(** Dynamic loading of .cmo *) -val dir_ml_load : string -> unit - -(** Dynamic interpretation of .ml *) -val dir_ml_use : string -> unit - (** List of modules linked to the toplevel *) val add_known_module : string -> unit val module_is_known : string -> bool |