- static disambiguation of Automath unified binders

[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 d64857d324cc878c4b216522e8ccbbf0ff7861f6..72ab254cd9193f5aff0981164e7bfe4cefab6ef1 100644 (file)
--- a/helm/software/helena/src/toplevel/top.ml
+++ b/helm/software/helena/src/toplevel/top.ml
@@ -229,7 +229,7 @@ let process_0 st entity =
          | AutEntity e -> 
             let err ast = {st with ast = ast} in
             let g ast e = process_1 {st with ast = ast} (CrgEntity e) in
-           AD.crg_of_aut err g st.ast e
+           AD.crg_of_aut err g st.kst st.ast e
          | TxtEntity e -> 
             let crr tst = {st with tst = tst} in
             let d tst e = process_1 {st with tst = tst} (CrgEntity e) in
@@ -328,7 +328,7 @@ let main =
       if !G.trace >= 1 then Y.utime_stamp "at exit"
    in
    let help = 
-      "Usage: helena [ -LPVXcdgiopqtx1 | -Ts <number> | -O <dir> | -hkr <string> ]* [ <file> ]*\n\n" ^
+      "Usage: helena [ -LPVXdgilopqtx1 | -Ts <number> | -O <dir> | -hkr <string> ]* [ <file> ]*\n\n" ^
       "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, \
        3 typing information, 4 reduction information\n\n" ^
       "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
@@ -340,14 +340,14 @@ let main =
    let help_V = " show version information" in
    let help_X = " clear options" in
    
-   let help_c = " read/write conversion constraints" in
    let help_d = " show summary information (requires trace >= 2)" in
    let help_g = " always expand global definitions" in
    let help_h = "<string>  set type hierarchy (default: \"Z1\")" in
    let help_i = " show local references by index" in
    let help_k = "<string>  set kernel version (default: \"brg\")" in
-   let help_o = " activate sort inclusion" in
-   let help_p = " preprocess source" in
+   let help_l = " disambiguate binders level (Automath)" in
+   let help_o = " activate sort inclusion (default: false)" in
+   let help_p = " preprocess source (Automath)" in
    let help_q = " disable quotation of identifiers" in
    let help_r = "<string>  set initial segment of URI hierarchy (default: empty)" in
    let help_s = "<number>  set translation stage (see above)" in
@@ -363,12 +363,12 @@ let main =
       ("-T", Arg.Int set_trace, help_T);
       ("-V", Arg.Unit print_version, help_V);
       ("-X", Arg.Unit clear_options, help_X);
-      ("-c", Arg.Set G.cc, help_c);
       ("-d", Arg.Unit set_summary, help_d);
       ("-g", Arg.Set G.expand, help_g);
       ("-h", Arg.String set_hierarchy, help_h);
       ("-i", Arg.Set G.indexes, help_i);
       ("-k", Arg.String set_kernel, help_k);
+      ("-l", Arg.Set G.cc, help_l);
       ("-o", Arg.Set G.si, help_o);
       ("-p", Arg.Unit set_preprocess, help_p);
       ("-q", Arg.Set G.unquote, help_q);