- we add the missing layer constraint on applicability condition

[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 bded35b3bc126ed1fd547678203a717c8d7a275d..e7f9158b1e05a8601cba1a517d091a7eac7fe342 100644 (file)
--- a/helm/software/helena/src/toplevel/top.ml
+++ b/helm/software/helena/src/toplevel/top.ml
@@ -97,8 +97,9 @@ let xlate_entity st entity = match !G.kernel, entity with
 let pp_progress e =
    let f _ na u =
       let s = U.string_of_uri u in
-      L.warn 2 (P.sprintf "[%u] <%s>" na.E.n_apix s)
+      L.warn 2 (P.sprintf "[%u] <%s>" na.E.n_apix s);
    in
+   Y.utime_stamp "intermediate";
    match e with
       | CrgEntity e -> E.common f e
       | BrgEntity e -> E.common f e
@@ -275,8 +276,7 @@ let process st name =
    let ich = open_in name in
    let lexbuf = Lexing.from_channel ich in 
    let st = process st lexbuf input in
-   close_in ich; 
-(*   if !G.cc then XL.export_csys st.kst.S.cc; *)
+   close_in ich;
    st, input
 
 let main = 
@@ -338,8 +338,9 @@ let main =
    in
    let help = 
       "Usage: helena [ -LPVXdgilopqtx1 | -Ts <number> | -MO <dir> | -m <file> | -ahkr <string> ]* [ <file> ]*\n\n" ^
-      "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 typing information,\n" ^
-      "              4 conversion information, 5 reduction information, 6 level disambiguation\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" ^
       "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
    in
    let help_L = " show lexer debug information" in 
@@ -392,4 +393,4 @@ let main =
       ("-t", Arg.Clear version, help_t);      
       ("-x", Arg.Set export, help_x);
       ("-1", Arg.Set streaming, help_1);      
-   ] process_file help;
+   ] process_file help