new semantics of the -g option completed

[helm.git] / helm / software / helena / src / toplevel / top.ml

diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml
index 3e7f8aa91d7c042e7a6cf32392b94514bb2a4f41..641871603acefb8c6d4c8522dcf83d4c73cd44b7 100644 (file)
--- a/helm/software/helena/src/toplevel/top.ml
+++ b/helm/software/helena/src/toplevel/top.ml
@@ -381,7 +381,7 @@ let main =
    let help_b = "<age>    [begin]     Begin trace at this global constant (default: first)" in
    let help_d = "         [data]      Show summary information (requires trace >= 2)" in
    let help_e = "<age>    [end]       End trace at this global constant (default: last)" in
-   let help_g = "         [global]    Always expand global definitions (default: false)" in
+   let help_g = "         [global]    Disable age-driven expansion of global definitions (default: enable)" in
    let help_h = "<string> [hierarchy] Set type hierarchy (default: \"Z1\")" in
    let help_i = "         [indexes]   Show local references by index" in
    let help_k = "<string> [kernel]    Set kernel version (default: \"V3\")" in
@@ -390,11 +390,11 @@ let main =
    let help_n = "         [names]     Show short constants (default: qualified constants)" in
    let help_o = "         [objects]   Export kernel entities (XML)" in
    let help_p = "<file>   [preamble]  Set preamble to this file (default: empty)" in
-   let help_q = "         [quote]     Disable quotation of identifiers (default: false)" in
+   let help_q = "         [quote]     Disable quotation of identifiers (default: enable)" in
    let help_r = "<string> [root]      Set initial segment of URI hierarchy (default: empty)" in
    let help_s = "<number> [stage]     Set translation stage (see above)" in
    let help_t = "         [type]      Type check (default: validate)" in
-   let help_u = "         [upsilon]   Activate type comparison by sort inclusion (default: false)" in
+   let help_u = "         [upsilon]   Activate type comparison by sort inclusion (default: deactivate)" in
    let help_x = "         [extended]  Use extended applications (Automath)" in
    let help_y = "         [infinity]  Use ∞-abstractions in contexts" in
    let help_0 = "         [zero]      Preprocess source (Automath)" in