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
  type pred_or_term =
      PoT_pred of Cil_types.predicate
    | PoT_term of Cil_types.term
  val is_used : Lscope.t -> Lscope.pred_or_term -> bool
end