sig
  type seq_t
  type proof_t
  type defs_t
  type rule_t
  type select_f = int -> Sigs.ABDRULE.proof_t -> int list
  type infrule_app =
      (Sigs.ABDRULE.seq_t * Tagpairs.t * Tagpairs.t) list * string
  type abdinfrule_f =
      Sigs.ABDRULE.seq_t -> Sigs.ABDRULE.defs_t -> Sigs.ABDRULE.defs_t list
  type abdbackrule_f =
      Sigs.ABDRULE.seq_t ->
      Sigs.ABDRULE.seq_t -> Sigs.ABDRULE.defs_t -> Sigs.ABDRULE.defs_t list
  type abdgenrule_f =
      Sigs.ABDRULE.seq_t ->
      Sigs.ABDRULE.defs_t ->
      (Sigs.ABDRULE.infrule_app * Sigs.ABDRULE.defs_t) list
  type t =
      int ->
      Sigs.ABDRULE.proof_t ->
      Sigs.ABDRULE.defs_t ->
      ((int list * Sigs.ABDRULE.proof_t) * Sigs.ABDRULE.defs_t) Blist.t
  val mk_abdinfrule : Sigs.ABDRULE.abdinfrule_f -> Sigs.ABDRULE.t
  val mk_abdbackrule :
    Sigs.ABDRULE.select_f -> Sigs.ABDRULE.abdbackrule_f -> Sigs.ABDRULE.t
  val mk_abdgenrule : Sigs.ABDRULE.abdgenrule_f -> Sigs.ABDRULE.t
  val fail : Sigs.ABDRULE.t
  val lift : Sigs.ABDRULE.rule_t -> Sigs.ABDRULE.t
  val compose : Sigs.ABDRULE.t -> Sigs.ABDRULE.t -> Sigs.ABDRULE.t
  val choice : Sigs.ABDRULE.t list -> Sigs.ABDRULE.t
  val attempt : Sigs.ABDRULE.t -> Sigs.ABDRULE.t
  val first : Sigs.ABDRULE.t list -> Sigs.ABDRULE.t
end