sig
  val ord : unit -> Libzipperposition.Ordering.t
  val selection_fun : unit -> Selection.t
  val set_selection_fun : Selection.t -> unit
  val set_ord : Libzipperposition.Ordering.t -> unit
  val signature : unit -> Libzipperposition.Signature.t
  val renaming : Libzipperposition.Substs.Renaming.t
  val compare :
    Libzipperposition.FOTerm.t ->
    Libzipperposition.FOTerm.t -> Libzipperposition.Comparison.t
  val select : Selection.t
  val renaming_clear : unit -> Libzipperposition.Substs.Renaming.t
  val lost_completeness : unit -> unit
  val is_completeness_preserved : unit -> bool
  val add_signature : Libzipperposition.Signature.t -> unit
  val find_signature :
    Libzipperposition.ID.t -> Libzipperposition.Type.t option
  val find_signature_exn : Libzipperposition.ID.t -> Libzipperposition.Type.t
  val declare : Libzipperposition.ID.t -> Libzipperposition.Type.t -> unit
  val on_new_symbol :
    (Libzipperposition.ID.t * Libzipperposition.Type.t) Signal.t
  val on_signature_update : Libzipperposition.Signature.t Signal.t
  module Lit :
    sig
      val from_hooks : unit -> Literal.Conv.hook_from list
      val add_from_hook : Literal.Conv.hook_from -> unit
      val to_hooks : unit -> Literal.Conv.hook_to list
      val add_to_hook : Literal.Conv.hook_to -> unit
      val of_form :
        Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t -> Literal.t
      val to_form :
        Literal.t -> Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t
    end
end