X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Ftop.ml;fp=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Ftop.ml;h=4c1ee1903bf0e8b6df9566f266344b329686f187;hb=3d23faf2969e2591db93f8bacc61952f3b66e2ca;hp=3556db37aed72a1ec6f68e66cb4669755d6d7109;hpb=3698de5ee6abc713534b0ee884e87e4046a087dd;p=helm.git

diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 3556db37a..4c1ee1903 100644
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -163,8 +163,8 @@ let process_0 f st entity =
 let rec process f book st = match book with
    | []           -> f st
    | entity :: tl -> 
-      process f tl (process_0 C.start st entity) 
-(*      process_0 (process f tl) st entity *) (* CPS variant of the above *)
+(* we exploit tail recursion rather than CPS *)
+      process f tl (process_0 C.start st entity)
 
 (****************************************************************************)