- the connections between the intermediate language and the "bag"

[helm.git] / helm / software / lambda-delta / src / complete_rg / crgOutput.ml

diff --git a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml
index c8d3bad88ec4448ba8590f2ad993e6f6eccd8fde..5d2faf90002ca3b631e7643170b35ef289a38790 100644 (file)
--- a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml
+++ b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml
@@ -44,11 +44,6 @@ let initial_counters = {
    uris = []; nodes = 0; xnodes = 0
 }
 
-let rec shift t = function
-   | D.ESort           -> t
-   | D.EBind (e, a, b) -> shift (D.TBind (a, b, t)) e
-   | D.EProj (e, a, d) -> shift (D.TProj (a, d, t)) e
-
 let rec count_term f c e = function
    | D.TSort _          -> 
       f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
@@ -75,7 +70,7 @@ let rec count_term f c e = function
       let f c = count_term f c e t in
       C.list_fold_right f (map1 e) vs c
    | D.TProj (a, d, t)  ->
-      count_term f c e (shift t d)
+      count_term f c e (D.tshift d t)
    | D.TBind (a, b, t)  -> 
       let f c e = count_term f c e t in
       count_binder f c e a b