diff options
| author | Gaëtan Gilbert | 2020-02-21 13:24:53 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-21 13:24:53 +0100 |
| commit | e1f2a1b97bb61e9c5ebaffda55a3be1ea3267c6b (patch) | |
| tree | f4c205e5d98700c0b118efe09498e22aff44adfb /toplevel/usage.ml | |
| parent | 4b6e6c6c187441f928921cbdd14093e296682f40 (diff) | |
| parent | 7489014fa6053c28e09852b0bf0602f2160cdda5 (diff) | |
Merge PR #11617: [init] Add `-boot` option to avoid binding `Coq.` prefix.
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: herbelin
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 6848862603..ba3deeb2f6 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -32,7 +32,8 @@ let print_usage_common co command = \n -coqlib dir set the coq standard library directory\ \n -exclude-dir f exclude subdirectories named f for option -R\ \n\ -\n -noinit start without loading the Init library\ +\n -boot don't bind the `Coq.` prefix to the default -coqlib dir\ +\n -noinit don't load Coq.Init.Prelude on start \ \n -nois (idem)\ \n -compat X.Y provides compatibility support for Coq version X.Y\ \n\ |