let f i = out (P.sprintf "+%i;" i) in
E.apix ignore f a
-let rec pp_term out = function
+let rec pp_term out st = function
| D.TSort (a, l) -> pp_attrs out a; out (P.sprintf "*%u" l)
| D.TLRef (a, i ) -> pp_attrs out a; out (P.sprintf "#%u" i)
| D.TGRef (a, u) -> pp_attrs out a; out (P.sprintf "$")
- | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out x; out ">."; pp_term out y
- | D.TAppl (a, x, y) -> pp_attrs out a; out "("; pp_term out x; out ")."; pp_term out y
- | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; out "."; pp_term out y
- | D.TProj (a, x, y) -> pp_attrs out a; out "{"; pp_lenv out x; out "}."; pp_term out y
+ | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out st x; out ">."; pp_term out st y
+ | D.TAppl (a, x, y) -> pp_attrs out a; out "("; pp_term out st x; out ")."; pp_term out st y
+ | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out st x; out "."; pp_term out st y
+ | D.TProj (a, x, y) -> pp_attrs out a; out "{"; pp_lenv out st x; out "}."; pp_term out st y
-and pp_bind out = function
+and pp_bind out st = function
| D.Abst (n, x) ->
- out "[:"; pp_term out x; out "]"; out (N.to_string n)
- | D.Abbr x -> out "[="; pp_term out x; out "]";
+ out "[:"; pp_term out st x; out "]"; out (N.to_string st n)
+ | D.Abbr x -> out "[="; pp_term out st x; out "]";
| D.Void -> out "[]"
-and pp_lenv out = function
+and pp_lenv out st = function
| D.ESort -> ()
- | D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y
- | D.EAppl (x, a, y) -> pp_lenv out x; out "("; pp_term out y; out ")"
- | D.EProj (x, a, y) -> pp_lenv out x; out "{"; pp_lenv out y; out "}"
+ | D.EBind (x, a, y) -> pp_lenv out st x; pp_attrs out a; pp_bind out st y
+ | D.EAppl (x, a, y) -> pp_lenv out st x; out "("; pp_term out st y; out ")"
+ | D.EProj (x, a, y) -> pp_lenv out st x; out "{"; pp_lenv out st y; out "}"