sig   type step = private {     size : int;     vars : Lang.F.Vars.t;     stmt : Cil_types.stmt option;     descr : string option;     deps : Property.t list;     warn : Warning.Set.t;     condition : Conditions.condition;   }   and condition =       Type of Lang.F.pred     | Have of Lang.F.pred     | When of Lang.F.pred     | Core of Lang.F.pred     | Init of Lang.F.pred     | Branch of Lang.F.pred * Conditions.sequence * Conditions.sequence     | Either of Conditions.sequence list   and sequence   type sequent = Conditions.sequence * Lang.F.pred   val step :     ?descr:string ->     ?stmt:Cil_types.stmt ->     ?deps:Property.t list ->     ?warn:Warning.Set.t -> Conditions.condition -> Conditions.step   val is_empty : Conditions.sequence -> bool   val vars_hyp : Conditions.sequence -> Lang.F.Vars.t   val vars_seq : Conditions.sequent -> Lang.F.Vars.t   val empty : Conditions.sequence   val seq_list : Conditions.step list -> Conditions.sequence   val seq_branch :     ?stmt:Cil_types.stmt ->     Lang.F.pred ->     Conditions.sequence -> Conditions.sequence -> Conditions.sequence   val append :     Conditions.sequence -> Conditions.sequence -> Conditions.sequence   val concat : Conditions.sequence list -> Conditions.sequence   val iter : (Conditions.step -> unit) -> Conditions.sequence -> unit   val iteri :     ?from:int ->     (int -> Conditions.step -> unit) -> Conditions.sequence -> unit   val condition : Conditions.sequence -> Lang.F.pred   val close : Conditions.sequent -> Lang.F.pred   type bundle   type 'a attributed =       ?descr:string ->       ?stmt:Cil_types.stmt ->       ?deps:Property.t list -> ?warn:Warning.Set.t -> 'a   val nil : Conditions.bundle   val occurs : Lang.F.var -> Conditions.bundle -> bool   val intersect : Lang.F.pred -> Conditions.bundle -> bool   val merge : Conditions.bundle list -> Conditions.bundle   val domain : Lang.F.pred list -> Conditions.bundle -> Conditions.bundle   val intros : Lang.F.pred list -> Conditions.bundle -> Conditions.bundle   val assume :     (?init:bool -> Lang.F.pred -> Conditions.bundle -> Conditions.bundle)     Conditions.attributed   val branch :     (Lang.F.pred ->      Conditions.bundle -> Conditions.bundle -> Conditions.bundle)     Conditions.attributed   val either :     (Conditions.bundle list -> Conditions.bundle) Conditions.attributed   val extract : Conditions.bundle -> Lang.F.pred list   val sequence : Conditions.bundle -> Conditions.sequence   exception Contradiction   class type simplifier =     object       method assume : Lang.F.pred -> unit       method copy : Conditions.simplifier       method fixpoint : unit       method infer : Lang.F.pred list       method name : string       method simplify_branch : Lang.F.pred -> Lang.F.pred       method simplify_goal : Lang.F.pred -> Lang.F.pred       method simplify_hyp : Lang.F.pred -> Lang.F.pred       method target : Lang.F.pred -> unit     end   val clean : Conditions.sequent -> Conditions.sequent   val filter : Conditions.sequent -> Conditions.sequent   val letify :     ?solvers:Conditions.simplifier list ->     Conditions.sequent -> Conditions.sequent   val pruning :     ?solvers:Conditions.simplifier list ->     Conditions.sequent -> Conditions.sequent end