X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgOutput.ml;h=1a0b0650e544cf8b9d79b711fcd1c9023483d58a;hb=32f2a8f8016b2c6c7fb88189fc0ea0c7f9336555;hp=fe496e25dc912ca2b0b82d6f41ed75b3cff7f9eb;hpb=cca5f6b7431b846b7bdcbf813632cb79580d5874;p=helm.git

diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml
index fe496e25d..1a0b0650e 100644
--- a/helm/software/lambda-delta/basic_rg/brgOutput.ml
+++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml
@@ -88,23 +88,23 @@ and count_term f c e = function
       let f c = B.push (f c) e b in
       count_term_binder f c e b
 
-let count_obj f c = function
+let count_entry f c = function
    | (_, u, B.Abst (_, w)) -> 
       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
       } in
       f c
 
-let count_item f c = function
-   | Some obj -> count_obj f c obj
+let count_unit f c = function
+   | Some entry -> count_entry f c entry
    | None     -> f c
 
 let print_counters f c =
@@ -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 
@@ -175,17 +175,17 @@ let id frm a =
 
 let rec pp_term c frm = function
    | B.Sort (_, h)             -> 
-      let err () = F.fprintf frm "@[*%u@]" h in
+      let err _ = F.fprintf frm "@[*%u@]" h in
       let f s = F.fprintf frm "@[%s@]" s in
       H.get_sort err f h 
    | B.LRef (_, i)             -> 
-      let err i = F.fprintf frm "@[#%u@]" i in
+      let err _ = F.fprintf frm "@[#%u@]" i in
       let f _ = function
          | B.Abst (a, _) 
 	 | B.Abbr (a, _)
 	 | B.Void a      -> F.fprintf frm "@[%a@]" id a
       in
-      if !O.indexes then err i else B.get err f c i
+      if !O.indexes then err () else B.get err f c i
    | B.GRef (_, s)             ->
       F.fprintf frm "@[$%s@]" (U.string_of_uri s)
    | B.Cast (_, u, t)          ->
@@ -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 ********************************************************)
@@ -275,7 +275,7 @@ and exp_bind c frm = function
    | B.Void a      ->
       F.fprintf frm "<Void%a/>" id a
 
-let exp_obj c frm = function
+let exp_entry c frm = function
    | _, u, B.Abst (a, w) -> 
       let str = U.string_of_uri u in
       let a = B.Name (true, U.name_of_uri u) :: a in
@@ -289,5 +289,5 @@ let exp_obj c frm = function
       let a = B.Name (true, U.name_of_uri u) :: a in
       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
+let export_entry frm entry =
+   F.fprintf frm "@,@[<v3>   %a@]@," (exp_entry B.empty_lenv) entry