new syntax of abstractions propagated to complete_rg

[helm.git] / helm / software / helena / src / automath / autCrg.ml

diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index a92b6fea98f44b696c10675650a5317bcafcdf40..c17b83f07a8f477e189518b84c580b59ccc86d33 100644 (file)
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -47,7 +47,7 @@ let alpha id =
 let add_abst cnt id aw w =
    let id = if !G.alpha <> "" then alpha id else id in
    let aw = {aw with E.n_name = Some (id, true); E.n_degr = succ aw.E.n_degr} in 
-   D.EBind (cnt, aw, D.Abst (N.two, w))
+   D.EBind (cnt, aw, D.Abst (false, N.two, w))
 
 let mk_lref f a i = f a (D.TLRef (a, i))
 
@@ -103,7 +103,7 @@ let get_cnt_relaxed f lst =
    get_cnt err f lst lst.node
 
 let push_abst f a w lenv =
-   let bw = D.Abst (N.infinite, w) in
+   let bw = D.Abst (false, N.infinite, w) in
    D.push_bind f a bw lenv
 
 let add_proj e t = match e with
@@ -135,7 +135,7 @@ let rec xlate_term f st lst y lenv = function
                   | _       -> assert false
                else N.infinite
             in
-           let b = D.Abst (l, ww) in
+           let b = D.Abst (false, l, ww) in
            let at = {at with E.n_name = name} in
            f at (D.TBind (at, b, tt))
         in