]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/toplevel/top.ml
- initial support for abstractions with explicit levels
[helm.git] / helm / software / lambda-delta / src / toplevel / top.ml
index 40a58673a01a837ba3255279671cad607ae07fc5..95ff41df34783cfc79a5d060927c57e7a6b4776e 100644 (file)
@@ -249,9 +249,10 @@ let process_0 st entity =
    if !preprocess then process_input f st entity else f st entity
 
 let process_nostreaming st lexbuf input =
+   let id x = x in
    let rec aux1 book = match entity_of_input lexbuf input with
       | NoEntity -> List.rev book
-      | e        -> aux1 (e :: book)   
+      | e        -> aux1 (id e :: book)   
    in
    let rec aux2 st = function
       | []           -> st
@@ -259,9 +260,12 @@ let process_nostreaming st lexbuf input =
    in
    aux2 st (aux1 [])
 
-let rec process_streaming st lexbuf input = match entity_of_input lexbuf input with
-   | NoEntity -> st
-   | e        -> process_streaming (process_0 st e) lexbuf input   
+let process_streaming st lexbuf input =
+   let rec aux st = match entity_of_input lexbuf input with
+      | NoEntity -> st
+      | e        -> aux (process_0 st e)
+   in
+   aux st
 
 (****************************************************************************)
 
@@ -275,7 +279,7 @@ let process st name =
 
 let main =
 try 
-   let version_string = "Helena 0.8.1 M - August 2010" in
+   let version_string = "Helena 0.8.1 M - October 2010" in
    let print_version () = L.warn (version_string ^ "\n"); exit 0 in
    let set_hierarchy s = 
       if H.set_graph s then () else