]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brgReduction.ml
some interfaces improved
[helm.git] / helm / software / lambda-delta / basic_rg / brgReduction.ml
index 71a0d1639f3986a1bed66ecb35203ece83210bc7..e6ea501423b65792c82c084c3c3bc696cc01f521 100644 (file)
@@ -18,7 +18,7 @@ module B = Brg
 module O = BrgOutput
 module E = BrgEnvironment
 
-type machine = {
+type kam = {
    c: B.lenv;
    s: (B.lenv * B.term) list;
    i: int
@@ -78,7 +78,7 @@ let rec step f ?(delta=false) ?(rt=false) m x =
         | e, _, b                        ->
            f m (Some (e, b)) x
       in
-      E.get_obj C.err f uri
+      E.get_entry C.err f uri
    | B.LRef (_, i)             ->
       let f c = function
         | B.Abbr (_, v)         ->
@@ -176,7 +176,7 @@ and ac_stacks err f m1 m2 =
 
 (* Interface functions ******************************************************)
 
-let empty_machine = { 
+let empty_kam = { 
    c = B.empty_lenv; s = []; i = 0
 }