diff options
| author | Maxime Dénès | 2017-03-22 00:36:51 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-22 00:36:51 +0100 |
| commit | 151286ec0c0887d212e7e85205352de4ddbf4bf2 (patch) | |
| tree | fc359fce2dbbfdc5250f9089079a8ad60cb1fbb4 /toplevel | |
| parent | 28d3bb3c8bddc63d038d8d55a34c928675fa9f7b (diff) | |
| parent | b087d133f7d6d091cce72190c05a9a09d5b37791 (diff) | |
Merge PR#482: [toplevel] Remove unusable option -notop
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 8 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
2 files changed, 3 insertions, 6 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index cc1c44fe31..c9a1f0def5 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -122,11 +122,10 @@ let engage () = let set_batch_mode () = batch_mode := true let toplevel_default_name = DirPath.make [Id.of_string "Top"] -let toplevel_name = ref (Some toplevel_default_name) +let toplevel_name = ref toplevel_default_name let set_toplevel_name dir = if DirPath.is_empty dir then error "Need a non empty toplevel module name"; - toplevel_name := Some dir -let unset_toplevel_name () = toplevel_name := None + toplevel_name := dir let remove_top_ml () = Mltop.remove () @@ -556,7 +555,6 @@ let parse_args arglist = if Coq_config.no_native_compiler then warning "Native compilation was disabled at configure time." else native_compiler := true - |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true |"-profile-ltac" -> Flags.profile_ltac := true |"-q" -> no_load_rc () @@ -628,7 +626,7 @@ let init_toplevel arglist = engage (); if (not !batch_mode || List.is_empty !compile_list) && Global.env_is_initial () - then Option.iter Declaremods.start_library !toplevel_name; + then Declaremods.start_library !toplevel_name; init_library_roots (); load_vernac_obj (); require (); diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 38ceacf5ec..66f782ffbe 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -30,7 +30,6 @@ let print_usage_channel co command = \n -R dir coqdir recursively map physical dir to logical coqdir\ \n -Q dir coqdir map physical dir to logical coqdir\ \n -top coqdir set the toplevel name to be coqdir instead of Top\ -\n -notop set the toplevel name to be the empty logical path\ \n -exclude-dir f exclude subdirectories named f for option -R\ \n\ \n -noinit start without loading the Init library\ |