some interfaces improved

[helm.git] / helm / software / lambda-delta / basic_ag / bagReduction.ml

diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml
index c2de019cd57628f8e250a239509d541340910ae8..628968befdd51b7beda755cf3e322e9beae926bd 100644 (file)
--- a/helm/software/lambda-delta/basic_ag/bagReduction.ml
+++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml
@@ -19,14 +19,14 @@ module S = BagSubstitution
 
 type machine = {
    i: int;
-   c: B.context;
+   c: B.lenv;
    s: B.term list
 }
 
 type whd_result =
    | Sort_ of int
    | LRef_ of int * B.term option
-   | GRef_ of B.obj
+   | GRef_ of B.entry
    | Bind_ of int * B.id * B.term * B.term
 
 type ho_whd_result =
@@ -44,14 +44,14 @@ let term_of_whdr = function
 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 empty_machine = {i = 0; c = B.empty_context; s = []}
+let empty_machine = {i = 0; c = B.empty_lenv; s = []}
 
 let inc m = {m with i = succ m.i}
 
@@ -83,8 +83,8 @@ let rec whd f c m x =
    match x with
    | B.Sort h                    -> f m (Sort_ h)
    | B.GRef uri                  ->
-      let f obj = f m (GRef_ obj) in
-      E.get_obj f uri
+      let f entry = f m (GRef_ entry) in
+      E.get_entry f uri
    | B.LRef i                    ->
       let f = function
          | B.Void   -> f m (LRef_ (i, None))