- bug fix in the static analyzer allows better Pi/forall separation (exportation...

[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 0f953949efff60ea83e2d5a3b9fc0784379e9b17..3e7f8aa91d7c042e7a6cf32392b94514bb2a4f41 100644 (file)
--- a/helm/software/helena/src/toplevel/top.ml
+++ b/helm/software/helena/src/toplevel/top.ml
@@ -219,7 +219,6 @@ let count_input st = function
 let version = ref true
 let preprocess = ref false
 let root = ref ""
-let export = ref false
 let st = ref (initial_status ())
 let streaming = ref false (* parsing style (temporary) *)
 
@@ -230,7 +229,7 @@ let process_2 st entity =
          let f = if !version then validate else type_check in f st entity
       else st
    in
-   if !export then export_entity st entity;
+   if !G.export then export_entity st entity;
    match st.mst with
      | None                    -> st
      | Some (export_entity, _) -> manager st export_entity entity
@@ -238,7 +237,7 @@ let process_2 st entity =
 let process_1 st entity = 
    if !G.ct >= 3 then pp_progress entity;
    let st = if !G.summary then count_entity st entity else st in
-   if !export && !G.stage = 1 then export_entity st entity;
+   if !G.export && !G.stage = 1 then export_entity st entity;
    if !G.stage >= 2 then process_2 st (xlate_entity st entity) else st 
 
 let process_0 st entity = 
@@ -322,7 +321,7 @@ let main =
       | s     -> L.warn level (KP.sprintf "Unknown manager: %s" s) 
    in
    let clear_options () =
-      export := false; preprocess := false;
+      preprocess := false;
       root := "";
       G.clear (); H.clear (); O.clear_reductions ();
       streaming := false;
@@ -363,7 +362,7 @@ let main =
       if !G.trace >= 1 then Y.utime_stamp "at exit"
    in
    let help = 
-      "Usage: helena [ -LPVXdgilnoqtux01 | -Ts <number> | -MO <dir> | -p <file> | -ahkmr <string> | -be <age> ]* [ <file> ]*\n\n" ^
+      "Usage: helena [ -LPVXdgilnoqtuxy01 | -Ts <number> | -MO <dir> | -p <file> | -ahkmr <string> | -be <age> ]* [ <file> ]*\n\n" ^
       "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 processed objects,\n" ^
       "              4 typing information, 5 conversion information, 6 reduction information,\n" ^
       "              7 level disambiguation\n\n" ^
@@ -396,7 +395,8 @@ let main =
    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_x = "         [extended]  Use extended applications (Automath)" 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 exit;
@@ -419,7 +419,7 @@ let main =
       ("-l", Arg.Set G.cc, help_l);
       ("-m", Arg.String set_manager, help_m);      
       ("-n", Arg.Set G.short, help_n);
-      ("-o", Arg.Set export, help_o);
+      ("-o", Arg.Set G.export, help_o);
       ("-p", Arg.String ((:=) G.preamble), help_p);
       ("-q", Arg.Set G.unquote, help_q);      
       ("-r", Arg.String ((:=) root), help_r);
@@ -427,6 +427,7 @@ let main =
       ("-t", Arg.Clear version, help_t);      
       ("-u", Arg.Set G.si, help_u);
       ("-x", Arg.Set G.extended, help_x);
+      ("-y", Arg.Set G.infinity, help_y);
       ("-0", Arg.Unit set_preprocess, help_0);
       ("-1", Arg.Set streaming, help_1);      
    ] process_file help