type 'a t = {ple0 : 'a;is_le : bool;dep : (Numbers.Q.t * 'a * bool) Util.MI.t;expl : Explanation.t;age : Numbers.Z.t;}module type S = sig ... endmodule FM
(P : Polynome.T with type r = Shostak.Combine.r) :
S with type p = P.tmodule type Container_SIG = sig ... endval get_current : unit -> (module Container_SIG)returns the current activated 'inequalities reasoner'. The default value is the Fourier-Motzkin module. When the selected reasoner is an external plugin, the first call of this function will attemp to dynamically load it *
val set_current : (module Container_SIG) -> unitsets a new 'inequalities reasoner'. This function is intended to be used by dynamically loaded plugins *