refactoring ...

[helm.git] / helm / software / lambda-delta / src / basic_ag / bagSubstitution.ml

diff --git a/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml b/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml
deleted file mode 100644 (file)
index f8c3478..0000000
--- a/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml
+++ /dev/null
@@ -1,48 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-module W = 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
-      lref_map f map v      
-   | Z.Abst w ->
-      let f w' = f (W.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)
-   | 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' = 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' = 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' = lref_map (f b') map u in 
-      lref_map_bind f map b
-
-(* Interface functions ******************************************************)
-
-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