]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml
we renamed the module abbreviations according to src/modules.ml
[helm.git] / helm / software / lambda-delta / src / basic_ag / bagSubstitution.ml
index ad75d63b83e06efbefed39b32d6f172ac044329c..46cd95c149ed6c8943b63241ed4316efbe818b0c 100644 (file)
       V_______________________________________________________________ *)
 
 module S = Share
-module B = Bag
+module Z = Bag
 
 (* Internal functions *******************************************************)
 
 let rec lref_map_bind f map b = match b with
-   | B.Abbr v ->
-      let f v' = f (S.sh1 v v' b B.abbr) in
+   | Z.Abbr v ->
+      let f v' = f (S.sh1 v v' b Z.abbr) in
       lref_map f map v      
-   | B.Abst w ->
-      let f w' = f (S.sh1 w w' b B.abst) in
+   | Z.Abst w ->
+      let f w' = f (S.sh1 w w' b Z.abst) in
       lref_map f map w
-   | B.Void   -> f b
+   | Z.Void   -> f b
 
 and lref_map f map t = match t with
-   | B.LRef i            -> 
-      let ii = map i in f (S.sh1 i ii t B.lref)
-   | B.GRef _            -> f t
-   | B.Sort _            -> f t
-   | B.Cast (w, u)       ->
-      let f w' u' = f (S.sh2 w w' u u' t B.cast) in
+   | Z.LRef i            -> 
+      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 (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
-   | B.Appl (w, u)       ->
-      let f w' u' = f (S.sh2 w w' u u' t B.appl) in
+   | Z.Appl (w, u)       ->
+      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
-   | B.Bind (l, id, b, u) ->
-      let f b' u' = f (S.sh2 b b' u u' t (B.bind l id)) in
+   | Z.Bind (l, id, b, u) ->
+      let f b' u' = f (S.sh2 b b' u u' t (Z.bind l id)) in
       let f b' = lref_map (f b') map u in 
       lref_map_bind f map b