- the disambiguation of unified binders continues

[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 0acd43336d090ee42a3c096d300287623036c296..d9649494e44391f1d537bdec73833ac834c1fd9c 100644 (file)
--- a/helm/software/helena/src/complete_rg/crg.ml
+++ b/helm/software/helena/src/complete_rg/crg.ml
@@ -113,3 +113,10 @@ let rec mem err f e b = match e with
    | EAppl (e, _, _) -> mem err f e b
    | EProj (e, _, d) -> 
       let err () = mem err f e b in mem err f d b
+
+let rec sta f = function
+   | ESort                     -> f ESort
+   | EBind (e, a, Abst (_, w)) -> sta (push_bind f a (Abst (N.one, w))) e
+   | EBind (e, a, b)           -> sta (push_bind f a b) e
+   | EAppl (e, a, v)           -> sta (push_appl f a v) e
+   | EProj (e, a, d)           -> let f d = sta (push_proj f a d) e in sta f d