X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2FbrgCrg.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2FbrgCrg.ml;h=f844c2e5114cec00d2cd7685d75f18249e9e2a44;hb=22fd9c98a22929f0319286c0693fcdaee43a72df;hp=32950e1cf557c5a55a8463752179224b75923d33;hpb=10d33a8c1be31d0c7aeccee8968fd5218ca2510a;p=helm.git

diff --git a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
index 32950e1cf..f844c2e51 100644
--- a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
+++ b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
@@ -12,6 +12,7 @@
 module C = Cps
 module E = Entity
 module J = Marks
+module N = Level
 module D = Crg
 module B = Brg
 
@@ -37,8 +38,8 @@ let rec xlate_term f = function
    | D.TProj (a, e, t)  ->
       let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
       xlate_term f t
-   | D.TBind (ab, D.Abst ws, D.TCast (ac, u, t)) ->
-      xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst ws, u), D.TBind (ab, D.Abst ws, t)))
+   | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
+      xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
    | D.TBind (a, b, t)  ->
       let f tt = f (xlate_bind tt a b) in xlate_term f t
 
@@ -46,19 +47,19 @@ and xlate_bind x a b =
    let f a ns = a, ns in
    let a, ns = E.get_names f a in 
    match b with
-      | D.Abst ws ->
+      | D.Abst (m, ws) ->
          let map x n w = 
-	    let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst ww, x) in 
+	    let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst (m, ww), x) in 
 	    xlate_term f w
 	 in
 	 List.fold_left2 map x ns ws 
-      | D.Abbr vs ->
+      | D.Abbr vs      ->
          let map x n v = 
 	    let f vv = B.Bind (n :: a, B.Abbr vv, x) in 
 	    xlate_term f v
 	 in
 	 List.fold_left2 map x ns vs
-      | D.Void _  ->
+      | D.Void _       ->
          let map x n = B.Bind (n :: a, B.Void, x) in
 	 List.fold_left map x ns
 
@@ -85,13 +86,13 @@ let rec xlate_bk_term f = function
       xlate_bk_bind f b
 
 and xlate_bk_bind f = function
-   | B.Abst t ->
-      let f tt = f (D.Abst [tt]) in
+   | B.Abst (n, t) ->
+      let f tt = f (D.Abst (n, [tt])) in
       xlate_bk_term f t
-   | B.Abbr t ->
+   | B.Abbr t      ->
       let f tt = f (D.Abbr [tt]) in
       xlate_bk_term f t
-   | B.Void   -> f (D.Void 1)
+   | B.Void        -> f (D.Void 1)
    
 (* interface functions ******************************************************)