some renaming and some interfaces improved

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

diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml
index eec76f62003685dbdbe12f48f8c57c0da4735ea4..47005ec6d4d1b227e2a5c5520f11abc1481c9155 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgOutput.ml
+++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml
@@ -93,10 +93,10 @@ let count_obj f c = function
       let c = {c with
          eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris
       } in
-      count_term f c B.empty_context w
+      count_term f c B.empty_lenv w
    | (_, _, B.Abbr (_, v)) ->  
       let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
-      count_term f c B.empty_context v
+      count_term f c B.empty_lenv v
    | (_, u, B.Void _)      ->
       let c = {c with 
          evoids = succ c.evoids; nodes = succ c.nodes; uris = u :: c.uris
@@ -164,7 +164,7 @@ let rename_bind f c = function
    | B.Abbr (a, v) -> let f a = f (B.abbr a v) in rename f c a
    | B.Void a      -> let f a = f (B.Void a) in rename f c a
 
-(* context/term pretty printing *********************************************)
+(* lenv/term pretty printing ************************************************)
 
 let id frm a =
    let f n = function 
@@ -209,7 +209,7 @@ let rec pp_term c frm = function
       let f a = B.push (f a) c (B.Void a) in
       rename f c a
 
-let pp_context frm c =
+let pp_lenv frm c =
    let pp_entry f c = function
       | B.Abst (a, w) -> 
          let f a = F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w; f () in
@@ -224,7 +224,7 @@ let pp_context frm c =
    B.rev_iter C.start pp_entry c
 
 let specs = {
-   L.pp_term = pp_term; L.pp_context = pp_context
+   L.pp_term = pp_term; L.pp_lenv = pp_lenv
 }
 
 (* term xml printing ********************************************************)
@@ -290,4 +290,4 @@ let exp_obj c frm = function
       F.fprintf frm "<VOID uri=%S%a/>" str id a
 
 let export_obj frm obj =
-   F.fprintf frm "@,@[<v3>   %a@]@," (exp_obj B.empty_context) obj
+   F.fprintf frm "@,@[<v3>   %a@]@," (exp_obj B.empty_lenv) obj