some renaming and 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 c8d8ddde9917060288ad5cc3694042539525d016..71a0d1639f3986a1bed66ecb35203ece83210bc7 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -19,8 +19,8 @@ module O = BrgOutput
 module E = BrgEnvironment
 
 type machine = {
-   c: B.context;
-   s: (B.context * B.term) list;
+   c: B.lenv;
+   s: (B.lenv * B.term) list;
    i: int
 }
 
@@ -29,12 +29,12 @@ type machine = {
 let level = 5
 
 let log1 s c t =
-   let sc, st = s ^ " in the context", "the term" in
-   L.log O.specs level (L.ct_items1 sc c st t)
+   let sc, st = s ^ " in the environment", "the term" in
+   L.log O.specs level (L.et_items1 sc c st t)
 
 let log2 s cu u ct t =
-   let s1, s2, s3 = s ^ " in the context", "the term", "and in the context" in
-   L.log O.specs level (L.ct_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+   let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in
+   L.log O.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
 
 let are_alpha_convertible err f t1 t2 =
    let rec aux f = function
@@ -177,7 +177,7 @@ and ac_stacks err f m1 m2 =
 (* Interface functions ******************************************************)
 
 let empty_machine = { 
-   c = B.empty_context; s = []; i = 0
+   c = B.empty_lenv; s = []; i = 0
 }
 
 let get err f m i =
@@ -200,8 +200,8 @@ let are_convertible err f ?(si=false) mu u mw w =
 
 let pp_term m frm t = O.specs.L.pp_term m.c frm t
 
-let pp_context frm m = O.specs.L.pp_context frm m.c
+let pp_lenv frm m = O.specs.L.pp_lenv frm m.c
 
 let specs = {
-   L.pp_term = pp_term; L.pp_context = pp_context
+   L.pp_term = pp_term; L.pp_lenv = pp_lenv
 }