sig
  exception InvalidDecl of string
  type cst
  type case
  type path_cell = private {
    path_cst : Ind_cst.cst;
    path_case : Ind_cst.case;
    path_clauses : ClauseContext.t list;
  }
  type path = Ind_cst.path_cell list
  type cover_set = Ind_cst.case list
  val case_equal : Ind_cst.case -> Ind_cst.case -> bool
  val case_compare : Ind_cst.case -> Ind_cst.case -> int
  val case_hash : Ind_cst.case -> int
  val pp_case : Ind_cst.case CCFormat.printer
  val case_to_term : Ind_cst.case -> Libzipperposition.FOTerm.t
  val case_is_rec : Ind_cst.case -> bool
  val case_is_base : Ind_cst.case -> bool
  val case_sub_constants : Ind_cst.case -> Ind_cst.cst Sequence.t
  val cover_set_cases :
    ?which:[ `All | `Base | `Rec ] ->
    Ind_cst.cover_set -> Ind_cst.case Sequence.t
  exception Payload_cst of Ind_cst.cst
  val as_cst : Libzipperposition.ID.t -> Ind_cst.cst option
  val as_cst_exn : Libzipperposition.ID.t -> Ind_cst.cst
  val is_cst : Libzipperposition.ID.t -> bool
  val on_new_cst : Ind_cst.cst Signal.t
  val declare_cst :
    ?cover_set_depth:int ->
    Libzipperposition.ID.t -> ty:Libzipperposition.Type.t -> Ind_cst.cst
  val cst_of_term : Libzipperposition.FOTerm.t -> Ind_cst.cst option
  val cst_of_id :
    Libzipperposition.ID.t -> Libzipperposition.Type.t -> Ind_cst.cst
  val declarations_of_cst :
    Ind_cst.cst ->
    (Libzipperposition.ID.t * Libzipperposition.Type.t) Sequence.t
  val cst_equal : Ind_cst.cst -> Ind_cst.cst -> bool
  val cst_compare : Ind_cst.cst -> Ind_cst.cst -> int
  val cst_hash : Ind_cst.cst -> int
  val cst_id : Ind_cst.cst -> Libzipperposition.ID.t
  val cst_to_term : Ind_cst.cst -> Libzipperposition.FOTerm.t
  val cst_ty : Ind_cst.cst -> Libzipperposition.Type.t
  val cst_same_type : Ind_cst.cst -> Ind_cst.cst -> bool
  val pp_cst : Ind_cst.cst CCFormat.printer
  val cst_depth : Ind_cst.cst -> int
  val cst_cover_set : Ind_cst.cst -> Ind_cst.cover_set option
  val find_cst_in_term : Libzipperposition.FOTerm.t -> Ind_cst.cst Sequence.t
  val is_sub_cst : Libzipperposition.ID.t -> bool
  val is_sub_cst_of : Libzipperposition.ID.t -> Ind_cst.cst -> bool
  val as_sub_cst_of :
    Libzipperposition.ID.t -> Ind_cst.cst -> Ind_cst.cst option
  val cover_set_sub_constants : Ind_cst.cover_set -> Ind_cst.cst Sequence.t
  val dominates : Ind_cst.cst -> Ind_cst.cst -> bool
  val path_equal : Ind_cst.path -> Ind_cst.path -> bool
  val path_compare : Ind_cst.path -> Ind_cst.path -> int
  val path_hash : Ind_cst.path -> int
  val path_empty : Ind_cst.path
  val path_cons :
    Ind_cst.cst ->
    Ind_cst.case -> ClauseContext.t list -> Ind_cst.path -> Ind_cst.path
  val path_length : Ind_cst.path -> int
  val path_dominates : Ind_cst.path -> Ind_cst.path -> bool
  val path_contains_cst : Ind_cst.path -> Ind_cst.cst -> bool
  val pp_path : Ind_cst.path CCFormat.printer
  val lits_of_path : Ind_cst.path -> Literals.t
  val max_depth_ : int Pervasives.ref
end