sig
  type emitted_status =
      True
    | False_if_reachable
    | False_and_reachable
    | Dont_know
  module Emitted_status :
    sig
      type t = emitted_status
      val ty : t Type.t
      val name : string
      val descr : t Descr.t
      val packed_descr : Structural_descr.pack
      val reprs : t list
      val equal : t -> t -> bool
      val compare : t -> t -> int
      val hash : t -> int
      val pretty_code : Format.formatter -> t -> unit
      val internal_pretty_code :
        Type.precedence -> Format.formatter -> t -> unit
      val pretty : Format.formatter -> t -> unit
      val varname : t -> string
      val mem_project : (Project_skeleton.t -> bool) -> t -> bool
      val copy : t -> t
    end
  exception Inconsistent_emitted_status of Property_status.emitted_status *
              Property_status.emitted_status
  val emit :
    Emitter.t ->
    hyps:Property.t list ->
    Property.t -> ?distinct:bool -> Property_status.emitted_status -> unit
  val emit_and_get :
    Emitter.t ->
    hyps:Property.t list ->
    Property.t ->
    ?distinct:bool ->
    Property_status.emitted_status -> Property_status.emitted_status
  val logical_consequence :
    Emitter.t -> Property.t -> Property.t list -> unit
  val legal_dependency_cycle : Emitter.t -> Property.Set.t -> unit
  val self : State.t
  type emitter_with_properties = private {
    emitter : Emitter.Usable_emitter.t;
    mutable properties : Property.t list;
    logical_consequence : bool;
  }
  type inconsistent = private {
    valid : Property_status.emitter_with_properties list;
    invalid : Property_status.emitter_with_properties list;
  }
  type status = private
      Never_tried
    | Best of Property_status.emitted_status *
        Property_status.emitter_with_properties list
    | Inconsistent of Property_status.inconsistent
  type t = status
  val ty : t Type.t
  val name : string
  val descr : t Descr.t
  val packed_descr : Structural_descr.pack
  val reprs : t list
  val equal : t -> t -> bool
  val compare : t -> t -> int
  val hash : t -> int
  val pretty_code : Format.formatter -> t -> unit
  val internal_pretty_code : Type.precedence -> Format.formatter -> t -> unit
  val pretty : Format.formatter -> t -> unit
  val varname : t -> string
  val mem_project : (Project_skeleton.t -> bool) -> t -> bool
  val copy : t -> t
  val get : Property.t -> Property_status.status
  val iter_on_statuses :
    (Property_status.emitter_with_properties ->
     Property_status.emitted_status -> unit) ->
    Property.t -> unit
  val fold_on_statuses :
    (Property_status.emitter_with_properties ->
     Property_status.emitted_status -> '-> 'a) ->
    Property.t -> '-> 'a
  module Consolidation :
    sig
      type pending =
          Property.Set.t Emitter.Usable_emitter.Map.t
          Emitter.Usable_emitter.Map.t
      type consolidated_status = private
          Never_tried
        | Considered_valid
        | Valid of Emitter.Usable_emitter.Set.t
        | Valid_under_hyp of Property_status.Consolidation.pending
        | Unknown of Property_status.Consolidation.pending
        | Invalid of Emitter.Usable_emitter.Set.t
        | Invalid_under_hyp of Property_status.Consolidation.pending
        | Invalid_but_dead of Property_status.Consolidation.pending
        | Valid_but_dead of Property_status.Consolidation.pending
        | Unknown_but_dead of Property_status.Consolidation.pending
        | Inconsistent of string
      type t = consolidated_status
      val ty : t Type.t
      val name : string
      val descr : t Descr.t
      val packed_descr : Structural_descr.pack
      val reprs : t list
      val equal : t -> t -> bool
      val compare : t -> t -> int
      val hash : t -> int
      val pretty_code : Format.formatter -> t -> unit
      val internal_pretty_code :
        Type.precedence -> Format.formatter -> t -> unit
      val pretty : Format.formatter -> t -> unit
      val varname : t -> string
      val mem_project : (Project_skeleton.t -> bool) -> t -> bool
      val copy : t -> t
      val get : Property.t -> t
      val get_conjunction : Property.t list -> t
    end
  module Feedback :
    sig
      type t =
          Never_tried
        | Considered_valid
        | Valid
        | Valid_under_hyp
        | Unknown
        | Invalid
        | Invalid_under_hyp
        | Invalid_but_dead
        | Valid_but_dead
        | Unknown_but_dead
        | Inconsistent
      val get : Property.t -> Property_status.Feedback.t
      val get_conjunction : Property.t list -> Property_status.Feedback.t
    end
  module Consolidation_graph :
    sig
      type t
      val get : Property.t -> Property_status.Consolidation_graph.t
      val dump :
        Property_status.Consolidation_graph.t -> Format.formatter -> unit
    end
  val iter : (Property.t -> unit) -> unit
  val fold : (Property.t -> '-> 'a) -> '-> 'a
  val register : Property.t -> unit
  val register_property_add_hook : (Property.t -> unit) -> unit
  val remove : Property.t -> unit
  val register_property_remove_hook : (Property.t -> unit) -> unit
  val merge : old:Property.t list -> Property.t list -> unit
  val automatically_proven : Property.t -> bool
end