sig
  type sname = SName of string
  type ('crterm, 'variable) type_constraint =
      CTrue of Positions.position
    | CDump of Positions.position
    | CEquation of Positions.position * 'crterm * 'crterm
    | CConjunction of ('crterm, 'variable) Constraint.type_constraint list
    | CLet of ('crterm, 'variable) Constraint.scheme list *
        ('crterm, 'variable) Constraint.type_constraint
    | CInstance of Positions.position * Constraint.sname * 'crterm
    | CDisjunction of ('crterm, 'variable) Constraint.type_constraint list
  and ('crterm, 'variable) scheme =
      Scheme of Positions.position * 'variable list * 'variable list *
        ('crterm, 'variable) Constraint.type_constraint *
        ('crterm * Positions.position) Misc.StringMap.t
  type variable = MultiEquation.variable
  type crterm = Constraint.variable CoreAlgebra.arterm
  type tconstraint =
      (Constraint.crterm, Constraint.variable) Constraint.type_constraint
  type tscheme = (Constraint.crterm, Constraint.variable) Constraint.scheme
  val cposition : ('a, 'b) Constraint.type_constraint -> Positions.position
  val ( =?= ) :
    Constraint.crterm ->
    Constraint.crterm -> Positions.position -> Constraint.tconstraint
  val ex :
    ?pos:Positions.position ->
    Constraint.variable list ->
    Constraint.tconstraint -> Constraint.tconstraint
  val ( <? ) :
    Constraint.sname ->
    Constraint.crterm -> Positions.position -> Constraint.tconstraint
  val ( ^ ) :
    Constraint.tconstraint ->
    Constraint.tconstraint -> Constraint.tconstraint
  val conj : Constraint.tconstraint list -> Constraint.tconstraint
  val exists :
    ?pos:Positions.position ->
    (Constraint.crterm -> Constraint.tconstraint) -> Constraint.tconstraint
  val exists3 :
    ?pos:Positions.position ->
    (Constraint.crterm ->
     Constraint.crterm -> Constraint.crterm -> Constraint.tconstraint) ->
    Constraint.tconstraint
  val fl :
    ?pos:Positions.position ->
    Constraint.variable list ->
    Constraint.tconstraint -> Constraint.tconstraint
  val exists_list :
    ?pos:Positions.position ->
    'a list ->
    (('a * Constraint.crterm) list -> Constraint.tconstraint) ->
    Constraint.tconstraint
  val forall_list :
    ?pos:Positions.position ->
    MultiEquation.tname list ->
    ((MultiEquation.tname * Constraint.crterm) list -> Constraint.tconstraint) ->
    Constraint.tconstraint
  val exists_set :
    ?pos:Positions.position ->
    Misc.StringSet.t ->
    ((Constraint.crterm * Positions.position) Misc.StringMap.t ->
     Constraint.tconstraint) ->
    Constraint.tconstraint
  val monoscheme :
    ?pos:Positions.position ->
    (Constraint.crterm * Positions.position) Misc.StringMap.t ->
    Constraint.tscheme
  val scheme :
    ?pos:Positions.position ->
    Constraint.variable list ->
    Misc.StringSet.t ->
    ((Constraint.crterm * Positions.position) Misc.StringMap.t ->
     Constraint.tconstraint) ->
    Constraint.tscheme
  val scheme' :
    ?pos:Positions.position ->
    Constraint.variable list ->
    Misc.StringSet.t ->
    Misc.StringSet.t ->
    ((Constraint.crterm * Positions.position) Misc.StringMap.t ->
     Constraint.tconstraint) ->
    Constraint.tscheme
end