sig
  type env = Qed.Pretty.Make(T).env
  val empty : env
  val closed : T.Vars.t -> env
  val marks : env -> T.marks
  val bind : string -> T.term -> env -> env
  val fresh : env -> T.term -> string * env
  val pp_tau : Format.formatter -> T.tau -> unit
  val pp_term : env -> Format.formatter -> T.term -> unit
  val pp_def : env -> Format.formatter -> T.term -> unit
end