aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9b58c9a65..cd376214a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -571,7 +571,6 @@ let parse_args arglist =
|"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ())
|"-require" -> add_require (next ())
|"-top" -> set_toplevel_name (dirpath_of_string (next ()))
- |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
|"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
|"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
|"-vio2vo" ->