- we added some syntactic sugar in the text parser

[helm.git] / helm / software / lambda-delta / toplevel / top.ml

diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 66fbed460c6a5135dfa981e90797abbadef5612e..6c6691354f65e1754330d9e46db95a88d8950ed5 100644 (file)
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -305,7 +305,7 @@ try
       flush_all ()
    in
    let help = 
-      "Usage: helena [ -Vcgijmopqrux | -Ss <number> | -hk <string> ] <file> ...\n\n" ^
+      "Usage: helena [ -Vcgijmopqux | -Ss <number> | -hkr <string> ] <file> ...\n\n" ^
       "Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \
        3 data information, 4 typing information, 5 reduction information\n\n" ^
        "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
@@ -315,7 +315,7 @@ try
 
    let help_c = " output conversion constraints" in
    let help_g = " always expand global definitions" in
-   let help_h = "<string>  set type hierarchy (default: Z2)" in
+   let help_h = "<string>  set type hierarchy (default: Z1)" in
    let help_i = " show local references by index" in
    let help_j = " show URI of processed kernel objects" in
    let help_k = "<string>  set kernel version (default: brg)" in