sig
  type t
  val empty : Conditions.??.t
  val vars : Conditions.??.t -> Lang.F.Vars.t
  val is_empty : Conditions.??.t -> bool
  val is_true : Conditions.??.t -> Qed.Logic.maybe
  val add : Conditions.step -> Conditions.??.t -> Conditions.??.t
  val factorize :
    Conditions.??.t ->
    Conditions.??.t -> Conditions.??.t * Conditions.??.t * Conditions.??.t
  val big_inter : Conditions.??.t list -> Conditions.??.t
  val diff : Conditions.??.t -> Conditions.??.t -> Conditions.??.t
  val freeze : Conditions.??.t -> Conditions.sequence
  val map : (Conditions.condition -> 'a) -> Conditions.??.t -> 'a list
end