X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_ag%2FbagSubstitution.ml;h=a8109c3ffbc82e9bbc6161696752ec11bfa08342;hb=2976c347e18717e691825ebdf73a5ce941c57d1b;hp=5585b5d6a25a7c135a11425987779957a97a87a7;hpb=bbc1c6ccb596693c46f4d75d7875b94c79f1d575;p=helm.git

diff --git a/helm/software/helena/src/basic_ag/bagSubstitution.ml b/helm/software/helena/src/basic_ag/bagSubstitution.ml
index 5585b5d6a..a8109c3ff 100644
--- a/helm/software/helena/src/basic_ag/bagSubstitution.ml
+++ b/helm/software/helena/src/basic_ag/bagSubstitution.ml
@@ -12,6 +12,8 @@
 module S = Share
 module Z = Bag
 
+IFDEF TYPE THEN
+
 (* Internal functions *******************************************************)
 
 let rec lref_map_bind f map b = match b with
@@ -36,8 +38,8 @@ and lref_map f map t = match t with
       let f w' u' = f (S.sh2 w w' u u' t Z.appl) in
       let f w' = lref_map (f w') map u in 
       lref_map f map w
-   | Z.Bind (a, l, b, u) ->
-      let f b' u' = f (S.sh2 b b' u u' t (Z.bind a l)) in
+   | Z.Bind (y, l, b, u) ->
+      let f b' u' = f (S.sh2 b b' u u' t (Z.bind y l)) in
       let f b' = lref_map (f b') map u in 
       lref_map_bind f map b
 
@@ -46,3 +48,5 @@ and lref_map f map t = match t with
 let subst f new_l old_l t =
    let map i = if i = old_l then new_l else i in
    if new_l = old_l then f t else lref_map f map t
+
+END