new syntax of abstractions propagated to complete_rg

[helm.git] / helm / software / helena / src / basic_ag / bagCrg.ml

diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml
index 6a83282b39088bcffc0421804ea2a38f8c727a67..08f342496f1badd4e580df9e724e6ad2a47bfd73 100644 (file)
--- a/helm/software/helena/src/basic_ag/bagCrg.ml
+++ b/helm/software/helena/src/basic_ag/bagCrg.ml
@@ -34,8 +34,8 @@ let rec xlate_term st f c = function
    | D.TProj (_, e, t) ->
       D.shift (xlate_term st f c) e t
 (* this case should be removed by improving alpha-conversion *)
-   | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
-      xlate_term st f c (D.TCast (ac, D.TBind (ab, D.Abst (N.minus st n 1, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
+   | D.TBind (ab, D.Abst (x, n, ws), D.TCast (ac, u, t)) ->
+      xlate_term st f c (D.TCast (ac, D.TBind (ab, D.Abst (x, N.minus st n 1, ws), u), D.TBind (ab, D.Abst (x, n, ws), t)))
    | D.TBind (a, b, t) ->
       let f cc =
          let a, l, b = List.hd cc in
@@ -45,13 +45,13 @@ let rec xlate_term st f c = function
       xlate_bind st f c a b
 
 and xlate_bind st f c a = function
-   | D.Abst (_, w) ->
+   | D.Abst (_, _, w) ->
       let f ww = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abst ww) in 
       xlate_term st f c w
-   | D.Abbr v      -> 
+   | D.Abbr v         -> 
       let f vv = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abbr vv) in
       xlate_term st f c v
-   | D.Void        ->
+   | D.Void           ->
       Z.push "xlate_bind" f c a (P.new_mark ()) Z.Void
 
 (* internal functions: bag to crg term **************************************)
@@ -78,7 +78,7 @@ let rec xlate_bk_term f c = function
 
 and xlate_bk_bind f c = function
    | Z.Abst t ->
-      let f tt = f (D.Abst (N.infinite, tt)) in
+      let f tt = f (D.Abst (false, N.infinite, tt)) in
       xlate_bk_term f c t
    | Z.Abbr t ->
       let f tt = f (D.Abbr tt) in