diff --git a/tools/coqdep/lib/args.ml b/tools/coqdep/lib/args.ml index 1e59e2ec96bd..85d2361cfd42 100644 --- a/tools/coqdep/lib/args.ml +++ b/tools/coqdep/lib/args.ml @@ -39,7 +39,7 @@ let warn_unknown_option = let usage () = let open Printf in - eprintf " usage: coqdep [options] +\n"; + eprintf " usage: rocq dep [options] +\n"; eprintf " options:\n"; eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; diff --git a/tools/coqdoc/cmdArgs.ml b/tools/coqdoc/cmdArgs.ml index 354192ed73fb..9eda3f398f18 100644 --- a/tools/coqdoc/cmdArgs.ml +++ b/tools/coqdoc/cmdArgs.ml @@ -12,7 +12,7 @@ open Common let banner () = - Printf.eprintf "This is coqdoc version %s\n" Coq_config.version; + Printf.eprintf "This is rocq doc version %s\n" Coq_config.version; flush stderr let normalize_path p = @@ -226,11 +226,11 @@ let args_options = Arg.align [ " First line comments of the form (** * ModuleName : text *) will be interpreted as subtitles"; "--inline-notmono", arg_set (fun p -> { p with inline_notmono = true }), " Use a proportional width font for inline code (possibly with a different color)"; - "--version", Arg.Unit (fun () -> banner()), " Display coqdoc version"; + "--version", Arg.Unit (fun () -> banner()), " Display rocq doc version"; ] let add_input_files f = prefs := { !prefs with files = what_file f :: !prefs.files } -let usage_msg = "coqdoc [options] ...\nAvailable options are:" +let usage_msg = "rocq doc [options] ...\nAvailable options are:" let single_hyphen_opts = ["-html"; "-latex"; "-texmacs"; "-raw"; "-dvi"; "-ps"; "-pdf"; "-stdout"; "-output"; "-directory"; "-gallina"; "-short"; "-light"; "-title"; "-body-only"; "-no-preamble"; "-with-header"; "-with-footer"; "-no-index"; "-multi-index"; "-index"; "-toc"; "-table-of-contents"; "-vernac-file"; "-tex-file"; "-preamble"; "-files-from"; "-files"; "-glob-from"; "-no-glob"; "-quiet"; "-verbose"; "-no-externals"; "-external"; "-coqlib_url"; "-coqlib"; "-latin1"; "-utf8"; "-charset"; "-inputenc"; "-interpolate"; "-raw-comments"; "-parse-comments"; "-plain-comments"; "-toc-depth"; "-no-lib-name"; "-lib-name"; "-lib-subtitles"; "-inline-notmono"; "-version"] diff --git a/tools/coqworkmgr/rocqworkmgr.ml b/tools/coqworkmgr/rocqworkmgr.ml index 98bf7726d1f5..45cdff6e6b79 100644 --- a/tools/coqworkmgr/rocqworkmgr.ml +++ b/tools/coqworkmgr/rocqworkmgr.ml @@ -158,7 +158,7 @@ let parse_args argv = "-j",Arg.Set_int max_tokens, "max number of concurrent jobs"; "-d",Arg.Set debug, "do not detach (debug)"] in let usage = - "Prints on stdout an env variable assignment to be picked up by coq\n"^ + "Prints on stdout an env variable assignment to be picked up by rocq\n"^ "instances in order to limit the maximum number of concurrent workers.\n"^ "The default value is 2.\n"^ "Usage:" in diff --git a/tools/rocqmakefile.ml b/tools/rocqmakefile.ml index 95ad50595686..836a7abaf750 100644 --- a/tools/rocqmakefile.ml +++ b/tools/rocqmakefile.ml @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(* Coq_makefile: automatically create a Makefile for a Coq development *) +(* rocq makefile: automatically create a Makefile for a Rocq development *) open CoqProject_file open Printf @@ -19,7 +19,7 @@ let usage_coq_makefile ~ok = let out = if ok then stdout else stderr in output_string out "Usage summary:\ \n\ -\ncoq_makefile .... [file.v] ... [file.ml[ig]?] ... [file.ml{lib,pack}]\ +\nrocq makefile .... [file.v] ... [file.ml[ig]?] ... [file.ml{lib,pack}]\ \n ... [-I dir] ... [-R physicalpath logicalpath]\ \n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ \n ... [-arg opt] ... [-docroot path] [-f file] [-o file]\ diff --git a/tools/rocqwc.mll b/tools/rocqwc.mll index 3d73fe7061ae..79aef23dad5a 100644 --- a/tools/rocqwc.mll +++ b/tools/rocqwc.mll @@ -8,10 +8,10 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(* coqwc - counts the lines of spec, proof and comments in Coq sources +(* rocq wc - counts the lines of spec, proof and comments in Coq sources * Copyright (C) 2003 Jean-Christophe FilliĆ¢tre *) -(*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source. +(*s {\bf rocq wc.} Counts the lines of spec, proof and comments in a Coq source. It assumes the files to be lexically well-formed. *) (*i*){ @@ -250,12 +250,12 @@ let process_file f = update_totals () with | Sys_error s -> - flush stdout; eprintf "coqwc: %s: %s\n" f s; flush stderr + flush stdout; eprintf "rocq wc: %s: %s\n" f s; flush stderr (*s Parsing of the command line. *) let usage () = - prerr_endline "usage: coqwc [options] [files]"; + prerr_endline "usage: rocq wc [options] [files]"; prerr_endline "Options are:"; prerr_endline " -p print percentage of comments"; prerr_endline " -s print only the spec size"; diff --git a/topbin/rocqnative.ml b/topbin/rocqnative.ml index 39add13a1af2..e1fe4fba5df2 100644 --- a/topbin/rocqnative.ml +++ b/topbin/rocqnative.ml @@ -292,7 +292,7 @@ struct let print_usage_channel co command = output_string co command; - output_string co "coqnative options are:\n"; + output_string co "rocq native-precompile options are:\n"; output_string co " -Q dir coqdir map physical dir to logical coqdir\ \n -R dir coqdir synonymous for -Q\ @@ -311,7 +311,7 @@ let print_usage_channel co command = let print_usage = print_usage_channel stderr let print_usage_coqnative () = - print_usage "Usage: coqnative file\n\n" + print_usage "Usage: rocq native-precompile file\n\n" let usage () = print_usage_coqnative (); diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index dc26ad8dce3c..c2a4bb504a8f 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -20,10 +20,10 @@ let coqc_init ((_,color_mode),_) injections ~opts = injections let coqc_specific_usage = Boot.Usage.{ - executable_name = "coqc"; + executable_name = "rocq compile"; extra_args = "file..."; extra_options = "\n\ -coqc specific options:\ +rocq compile specific options:\ \n -o f.vo use f.vo as the output file name\ \n -verbose compile and output the input file\ \n -noglob do not dump globalizations\ diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 1f797469f0ef..c1c03291a547 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -12,7 +12,7 @@ open Pp open Coqargs (** This file provides generic support for Coq executables + specific - support for the coqtop executable *) + support for the rocq repl executable *) let () = at_exit flush_all @@ -80,7 +80,7 @@ let start_coq custom args = custom.run ~opts custom_opts state (** ****************************************) -(** Specific support for coqtop executable *) +(** Specific support for rocq repl executable *) let ltac_debug_answer = let open DebugHook.Answer in function | Prompt prompt -> @@ -184,10 +184,10 @@ let coqtop_run ({ run_mode; color_mode },_) ~opts state = | Batch -> exit 0 let coqtop_specific_usage = Boot.Usage.{ - executable_name = "coqtop"; + executable_name = "rocq repl"; extra_args = ""; extra_options = "\n\ -coqtop specific options:\n\ +rocq repl specific options:\n\ \n -batch batch mode (exits after interpretation of command line)\ \n" }