Module Lscope

module Lscope: sig .. end

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 : t

val is_empty : t -> bool

val add : lscope_var -> t -> t

val get_all : t -> lscope_var list

type pred_or_term =

`\|`	`PoT_pred of Cil_types.predicate`
`\|`	`PoT_term of Cil_types.term`

val is_used : t -> pred_or_term -> bool