sig
  type derivation =
      Good of TypeCore.env * Derivations.judgement * Derivations.rule
    | Bad of TypeCore.env * Derivations.judgement * Derivations.rule list
  and rule = Derivations.rule_instance * Derivations.derivation list
  and rule_instance = string
  and judgement =
      JSubType of TypeCore.typ * TypeCore.typ
    | JSubVar of TypeCore.var * TypeCore.typ
    | JSubPerm of TypeCore.typ
    | JSubFloating of TypeCore.typ
    | JSubConstraint of TypeCore.mode_constraint
    | JEqual of TypeCore.typ * TypeCore.typ
    | JLt of TypeCore.typ * TypeCore.typ
    | JGt of TypeCore.typ * TypeCore.typ
    | JNothing
    | JAdd of TypeCore.typ
  type result = TypeCore.env option * Derivations.derivation
  val no_proof : TypeCore.env -> Derivations.judgement -> Derivations.result
  val apply_axiom :
    TypeCore.env ->
    Derivations.judgement ->
    Derivations.rule_instance -> TypeCore.env -> Derivations.result
  val try_several :
    TypeCore.env ->
    Derivations.judgement ->
    Derivations.rule_instance ->
    'a list ->
    (TypeCore.env -> 'a list -> 'a -> Derivations.result) ->
    Derivations.result
  val nothing :
    TypeCore.env -> Derivations.rule_instance -> Derivations.result
  val ( >>| ) :
    Derivations.result ->
    (TypeCore.env -> TypeCore.env option) -> TypeCore.env option
  val drop : TypeCore.env -> TypeCore.env option
  val drop_derivation : Derivations.result -> TypeCore.env option
  val is_good : Derivations.result -> bool
  type state
  val try_proof :
    TypeCore.env ->
    Derivations.judgement ->
    Derivations.rule_instance -> Derivations.state -> Derivations.result
  val premises :
    TypeCore.env ->
    (TypeCore.env -> Derivations.result) list -> Derivations.state
  val ( >>= ) :
    Derivations.result ->
    (TypeCore.env -> Derivations.state) -> Derivations.state
  val qed : TypeCore.env -> Derivations.state
  val fail : Derivations.state
  val ( >>~ ) :
    Derivations.state -> (TypeCore.env -> TypeCore.env) -> Derivations.state
end