sig
  type lscope_var =
      Lvs_let of Cil_types.logic_var * Cil_types.term
    | Lvs_quantif of Cil_types.term * Cil_types.relation *
        Cil_types.logic_var * Cil_types.relation * Cil_types.term
    | Lvs_formal of Cil_types.logic_var * Cil_types.logic_info
    | Lvs_global of Cil_types.logic_var * Cil_types.term
  type t
  val empty : Lscope.t
  val is_empty : Lscope.t -> bool
  val add : Lscope.lscope_var -> Lscope.t -> Lscope.t
  val get_all : Lscope.t -> Lscope.lscope_var list
  val is_used : Lscope.t -> Misc.pred_or_term -> bool
end