aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/usage.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index e69b21a195..732ad05b26 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -50,10 +50,10 @@ let print_usage_common co command =
\n -require-export lib, -re lib\
\n load and transitively import Coq library lib\
\n (equivalent to Require Export lib.)\
-\n -require-import-from root lib, -rifrom lib\
+\n -require-import-from root lib, -rifrom root lib\
\n load and import Coq library lib\
\n (equivalent to From root Require Import lib.)\
-\n -require-export-from root lib, -refrom lib\
+\n -require-export-from root lib, -refrom root lib\
\n load and transitively import Coq library lib\
\n (equivalent to From root Require Export lib.)\
\n\