aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0523ffd44..d64e3d979 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -389,8 +389,6 @@ let parse_args arglist =
|"-emacs" -> set_emacs ()
|"-filteropts" -> filter_opts := true
|"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
- |"--help-XML-protocol" ->
- Serialize.document Xml_printer.to_string_fmt; exit 0
|"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true
|"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet
|"-indices-matter" -> Indtypes.enforce_indices_matter ()