basic_rg: reduction was not tail recursive by mistake

[helm.git] / helm / software / lambda-delta / basic_rg / brgSubstitution.ml

diff --git a/helm/software/lambda-delta/basic_rg/brgSubstitution.ml b/helm/software/lambda-delta/basic_rg/brgSubstitution.ml
index e482b66c0bc4ac951171c555e0022f578fd4759b..4355376e85f26c17011ed29e80a0b15397bb865e 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgSubstitution.ml
+++ b/helm/software/lambda-delta/basic_rg/brgSubstitution.ml
@@ -29,10 +29,10 @@ let iter map d =
 let lift_map h _ a i =
    if i + h >= 0 then B.LRef (a, i + h) else assert false
 
-let lift g h d t =
-   if h = 0 then g t else g (iter (lift_map h) d t)
+let lift h d t =
+   if h = 0 then t else iter (lift_map h) d t
 
-let lift_bind g h d = function
-   | B.Void _ as b -> g b
-   | B.Abst (a, w) -> let g w = g (B.abst a w) in lift g h d w
-   | B.Abbr (a, v) -> let g v = g (B.abbr a v) in lift g h d v
+let lift_bind h d = function
+   | B.Void _ as b -> b
+   | B.Abst (a, w) -> B.abst a (lift h d w)
+   | B.Abbr (a, v) -> B.abbr a (lift h d v)