Module Core.RefineEnv

module D := CodeUnit.Domain
module Cell : sig ... end
type cell = (D.tp * D.con) Cell.t
type t
val init : t
val globally : t -> t
val locals : t -> cell Bwd.bwd
val size : t -> int
val get_local_tp : int -> t -> D.tp
val get_local : int -> t -> D.con
val resolve_local : Ident.t -> t -> int option
val local_cof_thy : t -> CodeUnit.CofThy.Disj.t
val pp_env : t -> Basis.Pp.env
val sem_env : t -> D.env
val restrict : CodeUnit.CofThy.cof list -> t -> t
val append_con : Ident.t -> D.con -> D.tp -> t -> t
val location : t -> Basis.LexingUtil.span option
val set_location : Basis.LexingUtil.span option -> t -> t
val dump : t Basis.Pp.printer