- new attributes system

[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 1bd5945031249fb9aaa208677b6f7fec016ad02c..9724290f930fae807383420ba90713a658ba5ec9 100644 (file)
--- a/helm/software/helena/src/basic_ag/bagCrg.ml
+++ b/helm/software/helena/src/basic_ag/bagCrg.ml
@@ -35,7 +35,7 @@ let rec xlate_term f c = function
       D.shift (xlate_term 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 f c (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
+      xlate_term f c (D.TCast (ac, D.TBind (ab, D.Abst (N.minus n 1, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
    | D.TBind (a, b, t) ->
       let f cc =
          let a, l, b = List.hd cc in
@@ -46,28 +46,28 @@ let rec xlate_term f c = function
 
 and xlate_bind f c a = function
    | D.Abst (_, w) ->
-      let f ww = Z.push "xlate_bind" f c a (J.new_location ()) (Z.Abst ww) in 
+      let f ww = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abst ww) in 
       xlate_term f c w
    | D.Abbr v      -> 
-      let f vv = Z.push "xlate_bind" f c a (J.new_location ()) (Z.Abbr vv) in
+      let f vv = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abbr vv) in
       xlate_term f c v
    | D.Void        ->
-      Z.push "xlate_bind" f c a (J.new_location ()) Z.Void
+      Z.push "xlate_bind" f c a (J.new_mark ()) Z.Void
 
 (* internal functions: bag to crg term **************************************)
 
 let rec xlate_bk_term f c = function
-   | Z.Sort h            -> f (D.TSort ([], h))
-   | Z.GRef s            -> f (D.TGRef ([], s))
+   | Z.Sort h            -> f (D.TSort (E.empty_node, h))
+   | Z.GRef s            -> f (D.TGRef (E.empty_node, s))
    | Z.LRef l            -> 
-       let f i = f (D.TLRef ([], i)) in
+       let f i = f (D.TLRef (E.empty_node, i)) in
        Z.nth C.err f l c
    | Z.Cast (u, t)  ->
-      let f tt uu = f (D.TCast ([], uu, tt)) in
+      let f tt uu = f (D.TCast (E.empty_node, uu, tt)) in
       let f tt = xlate_bk_term (f tt) c u in
       xlate_bk_term f c t 
    | Z.Appl (u, t)       ->
-      let f tt uu = f (D.TAppl ([], uu, tt)) in
+      let f tt uu = f (D.TAppl (E.empty_node, uu, tt)) in
       let f tt = xlate_bk_term (f tt) c u in
       xlate_bk_term f c t 
    | Z.Bind (a, l, b, t) ->