+ let help_a = "<string> [alpha] Set prefix of numeric identifiers (default: empty)" in
+ 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] 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
+ let help_l = " [layer] Disambiguate binders layer (Automath)" in
+ let help_m = "<string> [manager] Export kernel entities for this manager (see above, default: no manager)" in
+ 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] Quote identifiers (default: disable)" 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: 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
+ let help_1 = " [one] parse files with streaming policy" in
+ at_exit custom_exit;