module G = Options
module N = Level
module E = Entity
+module R = Alpha
module B = Brg
(* Internal functions *******************************************************)
in
aux (strip 0 3)
-let rename f e a = f a
-
let out_name och a =
let f n = function
| true -> P.fprintf och "%s" n
P.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp
| B.Bind (a, B.Abst (n, w), t) ->
let op, cp = if p then "(", ")" else "", "" in
- let f a =
- let ee = B.push e B.empty a (B.abst n w) in
- let binder = match N.to_string st n with
- | "1" -> "Π"
- | "2" -> "λ"
- | _ -> ok := false; "?"
- in
- P.fprintf och "%s%s%a:%a.%a%s"
- op binder out_name a (out_term st false e) w (out_term st false ee) t cp
+ let a = R.alpha B.mem e a in
+ let ee = B.push e B.empty a (B.abst n w) in
+ let binder = match N.to_string st n with
+ | "1" -> "Π"
+ | "2" -> "λ"
+ | _ -> ok := false; "?"
in
- rename f e a
+ P.fprintf och "%s%s%a:%a.%a%s"
+ op binder out_name a (out_term st false e) w (out_term st false ee) t cp
| B.Bind (a, B.Abbr v, t) ->
let op, cp = if p then "(", ")" else "", "" in
- let f a =
- let ee = B.push e B.empty a (B.abbr v) in
- P.fprintf och "%slet %a ≝ %a in %a%s"
- op out_name a (out_term st false e) v (out_term st false ee) t cp
- in
- rename f e a
+ let a = R.alpha B.mem e a in
+ let ee = B.push e B.empty a (B.abbr v) in
+ P.fprintf och "%slet %a ≝ %a in %a%s"
+ op out_name a (out_term st false e) v (out_term st false ee) t cp
| B.Bind (a, B.Void, t) -> C.err ()
(* Interface functions ******************************************************)