Container_SIG.Make
module P : Polynome.T with type r = Shostak.Combine.r
module P = P
type t = {
ple0 : P.t; |
is_le : bool; |
dep : (Numbers.Q.t * P.t * bool) AltErgoLib.Util.MI.t; |
expl : Explanation.t; |
age : Numbers.Z.t; |
}
module MINEQS : sig ... end
val current_age : unit -> Numbers.Z.t
val create_ineq : P.t -> P.t -> bool -> Expr.t option -> Explanation.t -> t
val print_inequation : Stdlib.Format.formatter -> t -> unit