- revision of ground_2 and basic_2

[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 673b3a0baf523434b8d52c74d51cf807f8e4a2f8..455eb6ed4547b193ca52becf1e6fcd4c0e07554e 100644 (file)
--- a/helm/software/helena/src/complete_rg/crg.ml
+++ b/helm/software/helena/src/complete_rg/crg.ml
@@ -73,7 +73,8 @@ let resolve_lref err f id lenv =
      | EAppl (tl, _, _)  -> aux i tl
      | EBind (tl, a, _)  ->
         let f id0 _ = if id0 = id then f a i else aux (succ i) tl in
-        E.name err f a 
+        let err () = aux (succ i) tl in
+        E.name err f a
      | EProj (tl, _, d)  -> append (aux i) tl d
    in
    aux 0 lenv
@@ -114,9 +115,13 @@ 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 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
+let replace f n0 e =
+   let rec aux f = function
+      | ESort                     -> f ESort
+      | EBind (e, a, Abst (n, w)) -> aux (push_bind f a (Abst (n0, w))) e
+      | EBind (e, a, b)           -> aux (push_bind f a b) e
+      | EAppl (e, a, v)           -> aux (push_appl f a v) e
+      | EProj (e, a, d)           -> let f d = aux (push_proj f a d) e in aux f d
+
+   in
+   aux f e