new syntax of abstractions propagated to complete_rg

[helm.git] / helm / software / helena / src / basic_rg / brgCrg.ml

diff --git a/helm/software/helena/src/basic_rg/brgCrg.ml b/helm/software/helena/src/basic_rg/brgCrg.ml
index dd7f3b1e597d9d0e16b15aa0d661c0cf6f05bcf9..1715494d49043309693f4fe944de619acc6ece03 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgCrg.ml
+++ b/helm/software/helena/src/basic_rg/brgCrg.ml
@@ -34,15 +34,15 @@ let rec xlate_term f = function
    | D.TBind (a, b, t)  -> 
       xlate_term (xlate_bind f a b) t
 
-and xlate_bind f a b x = match b with
-   | D.Abst (n, w) ->
-      let f ww = f (B.Bind (a, B.Abst (false, n, ww), x)) in 
+and xlate_bind f a b t = match b with
+   | D.Abst (x, n, w) ->
+      let f ww = f (B.Bind (a, B.Abst (x, n, ww), t)) in 
       xlate_term f w
-   | D.Abbr v      ->
-      let f vv = f (B.Bind (a, B.Abbr vv, x)) in 
+   | D.Abbr v         ->
+      let f vv = f (B.Bind (a, B.Abbr vv, t)) in 
       xlate_term f v
-   | D.Void        ->
-      f (B.Bind (a, B.Void, x))
+   | D.Void           ->
+      f (B.Bind (a, B.Void, t))
 
 (* internal functions: brg to crg term **************************************)
 
@@ -64,8 +64,8 @@ let rec xlate_bk_term f = function
       xlate_bk_term f t 
 
 and xlate_bk_bind f = function
-   | B.Abst (_, n, t) ->
-      let f tt = f (D.Abst (n, tt)) in
+   | B.Abst (x, n, t) ->
+      let f tt = f (D.Abst (x, n, tt)) in
       xlate_bk_term f t
    | B.Abbr t         ->
       let f tt = f (D.Abbr tt) in