aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/usage.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/usage.ml')
-rw-r--r--toplevel/usage.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index a87e61bc5..d5a5a7aec 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -24,7 +24,6 @@ let print_usage_channel co command =
-require f load Coq object file f.vo and import it (Require f.)
-opt run the native-code version of Coq or Coq_SearchIsos
- -full run the native-code version of Coq with all tactics
-image f specify an alternative binary image f
-bindir dir specify an alternative directory for the binaries
-libdir dir specify an alternative directory for the library