- the disambiguation of unified binders continues

[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 9724290f930fae807383420ba90713a658ba5ec9..6ad1c328458dd0ca3d43385acae31389e7b37023 100644 (file)
--- a/helm/software/helena/src/basic_ag/bagCrg.ml
+++ b/helm/software/helena/src/basic_ag/bagCrg.ml
@@ -18,39 +18,39 @@ module Z = Bag
 
 (* internal functions: crg to bag term **************************************)
 
-let rec xlate_term f c = function
+let rec xlate_term st f c = function
    | D.TSort (_, h)    -> f (Z.Sort h)
    | D.TGRef (_, s)    -> f (Z.GRef s)
    | D.TLRef (a, i)    ->
       let _, l, _ = List.nth c i in f (Z.LRef l)
    | D.TCast (_, u, t) ->
       let f tt uu = f (Z.Cast (uu, tt)) in
-      let f tt = xlate_term (f tt) c u in
-      xlate_term f c t
+      let f tt = xlate_term st (f tt) c u in
+      xlate_term st f c t
    | D.TAppl (_, v, t) ->
       let f tt vv = f (Z.Appl (vv, tt)) in
-      let f tt = xlate_term (f tt) c v in
-      xlate_term f c t
+      let f tt = xlate_term st (f tt) c v in
+      xlate_term st f c t
    | D.TProj (_, e, t) ->
-      D.shift (xlate_term f c) 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 f c (D.TCast (ac, D.TBind (ab, D.Abst (N.minus n 1, ws), u), D.TBind (ab, D.Abst (n, ws), 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 (a, b, t) ->
       let f cc =
          let a, l, b = List.hd cc in
          let f tt = f (Z.Bind (a, l, b, tt)) in
-         xlate_term f cc t
+         xlate_term st f cc t
       in
-      xlate_bind f c a b
+      xlate_bind st f c a b
 
-and xlate_bind f c a = function
+and xlate_bind st f c a = function
    | D.Abst (_, w) ->
       let f ww = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abst ww) in 
-      xlate_term f c w
+      xlate_term st f c w
    | D.Abbr v      -> 
       let f vv = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abbr vv) in
-      xlate_term f c v
+      xlate_term st f c v
    | D.Void        ->
       Z.push "xlate_bind" f c a (J.new_mark ()) Z.Void
 
@@ -87,7 +87,7 @@ and xlate_bk_bind f c = function
 
 (* interface functions ******************************************************)
 
-let bag_of_crg f t =
-   xlate_term f Z.empty_lenv t
+let bag_of_crg st f t =
+   xlate_term st f Z.empty_lenv t
 
 let crg_of_bag f t = xlate_bk_term f Z.empty_lenv t