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