sig
  val quantif_to_exp :
    Cil_types.kernel_function ->
    Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t
  val predicate_to_exp_ref :
    (Cil_types.kernel_function ->
     Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t)
    Pervasives.ref
end