diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 8 | ||||
| -rw-r--r-- | toplevel/coqtop_bin.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqtop_byte_bin.ml | 15 | ||||
| -rw-r--r-- | toplevel/coqtop_opt_bin.ml | 15 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
5 files changed, 37 insertions, 4 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 06b2ba41b..a1a07fce8 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -271,6 +271,11 @@ let get_cache opt = function | "force" -> Some Stm.AsyncOpts.Force | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 +let get_identifier opt s = + try Names.Id.of_string s + with CErrors.UserError _ -> + prerr_endline ("Error: valid identifier expected after option "^opt); exit 1 + let is_not_dash_option = function | Some f when String.length f > 0 && f.[0] <> '-' -> true | _ -> false @@ -466,6 +471,9 @@ let parse_args arglist : coq_cmdopts * string list = |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular oval true (next ()) + |"-mangle-names" -> + Namegen.set_mangle_names_mode (get_identifier opt (next ())); oval + |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 diff --git a/toplevel/coqtop_bin.ml b/toplevel/coqtop_bin.ml deleted file mode 100644 index 56aced92a..000000000 --- a/toplevel/coqtop_bin.ml +++ /dev/null @@ -1,2 +0,0 @@ -(* Main coqtop initialization *) -let () = Coqtop.start() diff --git a/toplevel/coqtop_byte_bin.ml b/toplevel/coqtop_byte_bin.ml index 7d8354ec3..0b65cebbb 100644 --- a/toplevel/coqtop_byte_bin.ml +++ b/toplevel/coqtop_byte_bin.ml @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + let drop_setup () = begin try (* Enable rectypes in the toplevel if it has the directive #rectypes *) @@ -18,4 +28,7 @@ let drop_setup () = ml_loop = (fun () -> Toploop.loop ppf); }) -let _ = drop_setup () +(* Main coqtop initialization *) +let _ = + drop_setup (); + Coqtop.start() diff --git a/toplevel/coqtop_opt_bin.ml b/toplevel/coqtop_opt_bin.ml index 410b4679a..ea4c0ea52 100644 --- a/toplevel/coqtop_opt_bin.ml +++ b/toplevel/coqtop_opt_bin.ml @@ -1,3 +1,16 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + let drop_setup () = Mltop.remove () -let _ = drop_setup () +(* Main coqtop initialization *) +let _ = + drop_setup (); + Coqtop.start() diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 07553a2ab..504ffa521 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -79,6 +79,7 @@ let print_usage_channel co command = \n -impredicative-set set sort Set impredicative\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ +\n -mangle-names x mangle auto-generated names using prefix x\ \n -time display the time taken by each command\ \n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ |