X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcomplete_rg%2Fcrg.ml;fp=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcomplete_rg%2Fcrg.ml;h=a250d3edda087b68285d7bc1d7100b1a294b7d59;hb=2cf2e883f91164ce614bdc86b5c5e2419b98f68d;hp=ea3ec54bfc4b101799e1b59ca9316ddfe010f598;hpb=98fef490e55d1d780e8c0bb19de0218e08ae73b1;p=helm.git

diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml
index ea3ec54bf..a250d3edd 100644
--- a/helm/software/helena/src/complete_rg/crg.ml
+++ b/helm/software/helena/src/complete_rg/crg.ml
@@ -115,13 +115,28 @@ let rec mem err f e b = match e with
    | EProj (e, _, d)    -> 
       let err () = mem err f e b in mem err f d b
 
-let replace f n0 e =
+let set_layer f n0 e =
    let rec aux f = function
       | ESort                        -> f ESort
       | EBind (e, a, Abst (r, n, w)) -> aux (push_bind f a (Abst (r, n0, w))) e
       | EBind (e, a, b)              -> aux (push_bind f a b) e
       | EAppl (e, a, x, v)           -> aux (push_appl f a x v) e
       | EProj (e, a, d)              -> let f d = aux (push_proj f a d) e in aux f d
+   in
+   aux f e
 
+let set_attrs f a0 e =
+   let rec aux f = function
+      | ESort              -> f ESort
+      | EBind (e, a, b)    -> 
+         let a = E.compose a a0 in
+         aux (push_bind f a b) e
+      | EAppl (e, a, x, v) ->
+         let a = E.compose a a0 in
+         aux (push_appl f a x v) e
+      | EProj (e, a, d)    ->
+         let a = E.compose a a0 in
+         let f d = aux (push_proj f a d) e in
+         aux f d
    in
    aux f e