From 52cc1e4d8574f6738caa1f7bf19bdd1945e5537e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 11 Mar 2021 19:57:38 +0100
Subject: noglob/dumpglob should be in coqc specific usage

Fix #13930
---
 sysinit/usage.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'sysinit')

diff --git a/sysinit/usage.ml b/sysinit/usage.ml
index d00b916f23..5886b1c5b5 100644
--- a/sysinit/usage.ml
+++ b/sysinit/usage.ml
@@ -73,8 +73,6 @@ let print_usage_common co command =
 \n  -debug                 debug mode (implies -bt)\
 \n  -xml-debug             debug mode and print XML messages to/from coqide\
 \n  -diffs (on|off|removed) highlight differences between proof steps\
-\n  -noglob                do not dump globalizations\
-\n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
 \n  -impredicative-set     set sort Set impredicative\
 \n  -allow-sprop           allow using the proof irrelevant SProp sort\
 \n  -disallow-sprop        forbid using the proof irrelevant SProp sort\
-- 
cgit v1.2.3