- bug fix in the static analyzer allows better Pi/forall separation (exportation...

[helm.git] / helm / software / helena / src / complete_rg / crg.ml

diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml
index ea3ec54bfc4b101799e1b59ca9316ddfe010f598..a250d3edda087b68285d7bc1d7100b1a294b7d59 100644 (file)
--- 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