2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
17 (* Internal functions *******************************************************)
19 let rec lref_map_bind f map b = match b with
21 let f v' = f (S.sh1 v v' b Z.abbr) in
24 let f w' = f (S.sh1 w w' b Z.abst) in
28 and lref_map f map t = match t with
30 let ii = map i in f (S.sh1 i ii t Z.lref)
34 let f w' u' = f (S.sh2 w w' u u' t Z.cast) in
35 let f w' = lref_map (f w') map u in
38 let f w' u' = f (S.sh2 w w' u u' t Z.appl) in
39 let f w' = lref_map (f w') map u in
41 | Z.Bind (y, l, b, u) ->
42 let f b' u' = f (S.sh2 b b' u u' t (Z.bind y l)) in
43 let f b' = lref_map (f b') map u in
46 (* Interface functions ******************************************************)
48 let subst f new_l old_l t =
49 let map i = if i = old_l then new_l else i in
50 if new_l = old_l then f t else lref_map f map t