X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgOutput.ml;h=662a71988d5a3182579c9ee3bb6b2fd82305f5d3;hb=8049c166a37789d7a1b1ca1c3a1174712bbf87ba;hp=eec76f62003685dbdbe12f48f8c57c0da4735ea4;hpb=0dc347a7742e40a828fa98acba70078dd2d7cbd5;p=helm.git
diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml
index eec76f620..662a71988 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_entity 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
@@ -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 "" 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 "" str id a
-let export_obj frm obj =
- F.fprintf frm "@,@[ %a@]@," (exp_obj B.empty_context) obj
+let export_entry frm entry =
+ F.fprintf frm "@,@[ %a@]@," (exp_entry B.empty_lenv) entry