new options activated

[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 08f342496f1badd4e580df9e724e6ad2a47bfd73..b9ce1d3447e0b26b7d52a1f07862c1eb768818ab 100644 (file)
--- a/helm/software/helena/src/basic_ag/bagCrg.ml
+++ b/helm/software/helena/src/basic_ag/bagCrg.ml
@@ -19,15 +19,15 @@ module Z = Bag
 (* internal functions: crg to bag term **************************************)
 
 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)    ->
+   | 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) ->
+   | D.TCast (_, u, t)    ->
       let f tt uu = f (Z.Cast (uu, tt)) in
       let f tt = xlate_term st (f tt) c u in
       xlate_term st f c t
-   | D.TAppl (_, v, t) ->
+   | D.TAppl (_, _, v, t) ->
       let f tt vv = f (Z.Appl (vv, tt)) in
       let f tt = xlate_term st (f tt) c v in
       xlate_term st f c t
@@ -36,7 +36,7 @@ let rec xlate_term st f c = function
 (* this case should be removed by improving alpha-conversion *)
    | 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) ->
+   | 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
@@ -67,7 +67,7 @@ let rec xlate_bk_term f c = function
       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 (E.empty_node, uu, tt)) in
+      let f tt uu = f (D.TAppl (E.empty_node, true, 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) ->