sig
  type t
  module Mode :
    sig
      type t = Context | Internals | None
      val value : Context.Mode.t Pervasives.ref
      val set : Context.Mode.t -> ('a -> 'b) -> 'a -> 'b
    end
  val pp : Context.t Pretty.printer
  val eq : Context.t -> Context.t -> bool
  val empty : Context.t
  val ctxt_of : Context.t -> Atom.t list
  val partition_of : Context.t -> Partition.t
  val eqs_of : Context.t -> Combine.E.t
  val config_of : Context.t -> Combine.E.t * Partition.t
  val upper_of : Context.t -> int
  module Status :
    sig
      type 'a t = Valid of Jst.t | Inconsistent of Jst.t | Ok of 'a
      val pp : 'a Pretty.printer -> 'a Context.Status.t Pretty.printer
    end
  val add : Context.t -> Atom.t -> Context.t Context.Status.t
  val statistics : bool Pervasives.ref
  val verbose : bool Pervasives.ref
  val coi_enabled : int Pervasives.ref
  val semantic_coi_min : int Pervasives.ref
  val syntactic_coi_min : int Pervasives.ref
  val addl : Context.t -> Atom.t list -> Context.t Context.Status.t
  val is_inconsistent : Context.t -> Atom.t list -> bool
  val is_valid : Context.t -> Atom.t list -> bool
  val check_sat : Context.t -> Context.t option
  val diff : Context.t -> Context.t -> Context.t
end