X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fdual_rg%2Fdrg.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fdual_rg%2Fdrg.ml;h=b20bdb3d387468fccf6c7436ec34ea3c0cdcb403;hb=6753156ae1618ef3fc7ff401808f769abd9eb03d;hp=ac4021c08db2a4a8e99b1bf6dcb288d6f932c98f;hpb=8134330933e377a344b5ee38890198dc0b653428;p=helm.git

diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml
index ac4021c08..b20bdb3d3 100644
--- a/helm/software/lambda-delta/dual_rg/drg.ml
+++ b/helm/software/lambda-delta/dual_rg/drg.ml
@@ -57,7 +57,7 @@ let resolve_lref err f id lenv =
      | ESort            -> err ()
      | EBind (tl, a, _) ->
         let err kk = aux f (succ i) (k + kk) tl in
-	let f j = f i j k in
+	let f j = f i j (k + j) in
 	Entity.resolve err f id a
      | EProj _          -> assert false (* TODO *)
    in
@@ -65,6 +65,9 @@ let resolve_lref err f id lenv =
 
 let rec get_name err f i j = function
    | ESort                      -> err i
+   | EBind (tl, a, Abst [])     -> get_name err f i j tl
+   | EBind (tl, a, Abbr [])     -> get_name err f i j tl
+   | EBind (tl, a, Void 0)      -> get_name err f i j tl
    | EBind (_, a, _) when i = 0 -> 
       let err () = err i in
       Entity.get_name err f j a