Micromega_plugin (coq-core.Micromega

module Certificate : sig ... end

module Coq_micromega : sig ... end

module G_micromega : sig ... end

module Itv : sig ... end

module Linsolve : sig ... end

The purpose of the solver is to generate *all* the integer solutions of a system of linear equations of the following form: 1- all the variables are positive 2- all the coefficients are positive

module Micromega : sig ... end

module Mutils : sig ... end

module NumCompat : sig ... end

module Persistent_cache : sig ... end

module Polynomial : sig ... end

module Simplex : sig ... end

Profiling

module Sos : sig ... end

module Sos_lib : sig ... end

module Sos_types : sig ... end

module Vect : sig ... end