some interfaces improved

[helm.git] / helm / software / lambda-delta / basic_rg / brgReduction.ml

diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index 1ae73652d7d9f0778cba8ec7b6705bd5ad3319a0..5dff4647b43db3bd06f56153f146e443a4660dd8 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -20,9 +20,9 @@ module O = BrgOutput
 module E = BrgEnvironment
 
 type kam = {
-   e: B.lenv;
-   s: (B.lenv * B.term) list;
-   i: int
+   e: B.lenv;                 (* environment *)
+   s: (B.lenv * B.term) list; (* stack       *)
+   d: int                     (* depth       *)
 }
 
 (* Internal functions *******************************************************)
@@ -122,12 +122,12 @@ let rec step st m x =
 
 let push m a b = 
    assert (m.s = []);
-   let a, i = match b with
-      | B.Abst _ -> Y.Apix m.i :: a, succ m.i
-      | b        -> a, m.i
+   let a, d = match b with
+      | B.Abst _ -> Y.Apix m.d :: a, succ m.d
+      | b        -> a, m.d
    in
    let e = B.push m.e m.e a b in
-   {m with e = e; i = i}
+   {m with e = e; d = d}
 
 let rec ac_nfs st (m1, r1, u) (m2, r2, t) =
    log2 "Now converting nfs" m1.e u m2.e t;
@@ -180,7 +180,7 @@ and ac_stacks st m1 m2 =
 (* Interface functions ******************************************************)
 
 let empty_kam = { 
-   e = B.empty; s = []; i = 0
+   e = B.empty; s = []; d = 0
 }
 
 let get m i =