sig   val split :     (WpPropId.prop_id -> '-> unit) -> WpPropId.prop_id -> 'Bag.t -> unit   type proof   val create_proof : WpPropId.prop_id -> WpAnnot.proof   val add_proof :     WpAnnot.proof -> WpPropId.prop_id -> Property.t list -> unit   val is_composed : WpAnnot.proof -> bool   val is_proved : WpAnnot.proof -> bool   val target : WpAnnot.proof -> Property.t   val dependencies : WpAnnot.proof -> Property.t list   val filter_status : WpPropId.prop_id -> bool   val get_called_preconditions_at :     Cil_types.kernel_function -> Cil_types.stmt -> Property.t list   val get_called_post_conditions :     Cil_types.kernel_function -> Property.t list   val get_called_exit_conditions :     Cil_types.kernel_function -> Property.t list   val get_called_assigns : Cil_types.kernel_function -> Property.t list   type asked_assigns = NoAssigns | OnlyAssigns | WithAssigns   val get_id_prop_strategies :     model:Model.t ->     ?assigns:WpAnnot.asked_assigns -> Property.t -> WpStrategy.strategy list   val get_call_pre_strategies :     model:Model.t -> Cil_types.stmt -> WpStrategy.strategy list   val get_function_strategies :     model:Model.t ->     ?assigns:WpAnnot.asked_assigns ->     ?bhv:string list ->     ?prop:string list -> Kernel_function.t -> WpStrategy.strategy list end