- we are moving from old (patched) management of sort inclusion

[helm.git] / helm / software / helena / src / basic_ag / bagSubstitution.ml

diff --git a/helm/software/helena/src/basic_ag/bagSubstitution.ml b/helm/software/helena/src/basic_ag/bagSubstitution.ml
index f8c34789208be7ab19673e302966f3d09564c60a..5585b5d6a25a7c135a11425987779957a97a87a7 100644 (file)
--- a/helm/software/helena/src/basic_ag/bagSubstitution.ml
+++ b/helm/software/helena/src/basic_ag/bagSubstitution.ml
@@ -9,35 +9,35 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module W = Share
+module S = Share
 module Z = Bag
 
 (* Internal functions *******************************************************)
 
 let rec lref_map_bind f map b = match b with
    | Z.Abbr v ->
-      let f v' = f (W.sh1 v v' b Z.abbr) in
+      let f v' = f (S.sh1 v v' b Z.abbr) in
       lref_map f map v      
    | Z.Abst w ->
-      let f w' = f (W.sh1 w w' b Z.abst) in
+      let f w' = f (S.sh1 w w' b Z.abst) in
       lref_map f map w
    | Z.Void   -> f b
 
 and lref_map f map t = match t with
    | Z.LRef i            -> 
-      let ii = map i in f (W.sh1 i ii t Z.lref)
+      let ii = map i in f (S.sh1 i ii t Z.lref)
    | Z.GRef _            -> f t
    | Z.Sort _            -> f t
    | Z.Cast (w, u)       ->
-      let f w' u' = f (W.sh2 w w' u u' t Z.cast) in
+      let f w' u' = f (S.sh2 w w' u u' t Z.cast) in
       let f w' = lref_map (f w') map u in 
       lref_map f map w
    | Z.Appl (w, u)       ->
-      let f w' u' = f (W.sh2 w w' u u' t Z.appl) in
+      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 (W.sh2 b b' u u' t (Z.bind a l)) in
+      let f b' u' = f (S.sh2 b b' u u' t (Z.bind a l)) in
       let f b' = lref_map (f b') map u in 
       lref_map_bind f map b