functor
  (X : Sig.X) (P : sig
                     type r = X.r
                     type t
                     val compare : t -> t -> int
                     val hash : t -> int
                     val create : (Num.num * r) list -> Num.num -> Ty.t -> t
                     val add : t -> t -> t
                     val sub : t -> t -> t
                     val mult : t -> t -> t
                     val mult_const : Num.num -> t -> t
                     val div : t -> t -> t * bool
                     val modulo : t -> t -> t
                     val is_empty : t -> bool
                     val find : r -> t -> Num.num
                     val choose : t -> Num.num * r
                     val subst : r -> t -> t -> t
                     val remove : r -> t -> t
                     val to_list : t -> (Num.num * r) list * Num.num
                     val print : Format.formatter -> t -> unit
                     val type_info : t -> Ty.t
                     val is_monomial : t -> (Num.num * r * Num.num) option
                     val ppmc_denominators : t -> Num.num
                     val pgcd_numerators : t -> Num.num
                     val normal_form : t -> t * Num.num * Num.num
                     val normal_form_pos : t -> t * Num.num * Num.num
                     val poly_of : r -> t
                     val alien_of : t -> r
                   end) ->
  sig
    type t
    type r = X.r
    val empty : unit -> t
    val assume : t -> r Sig.input list -> t * r Sig.result
    val query : t -> r Sig.input -> Sig.answer
    val case_split : t -> (r Literal.view * Explanation.t * Num.num) list
    val add : t -> r -> t
  end