sig
  type 'a polynomial_context
  type 'a t
  val mk_context :
    'a Syntax.context -> 'a SrkSimplify.TermPolynomial.polynomial_context
  val of_term :
    'a SrkSimplify.TermPolynomial.polynomial_context ->
    'a Syntax.term -> 'a SrkSimplify.TermPolynomial.t
  val term_of :
    'a SrkSimplify.TermPolynomial.polynomial_context ->
    'a SrkSimplify.TermPolynomial.t -> 'a Syntax.term
end