X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fcomplete_rg%2FcrgOutput.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fcomplete_rg%2FcrgOutput.ml;h=5d2faf90002ca3b631e7643170b35ef289a38790;hb=a5709dff43233c041f77a4ee4b7f2df1a3c51ab6;hp=c8d3bad88ec4448ba8590f2ad993e6f6eccd8fde;hpb=f3f6b451707a3feb8245717e3fa7ca25df0ce8ef;p=helm.git

diff --git a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml
index c8d3bad88..5d2faf900 100644
--- 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