The Micromega plugin is a plugin for the Rocq Prover providing
(semi)decision procedures for arithmetic.
End users can use it through tactics like lra in libraries using the plugin.
Information on how to build and install from sources can be found in
INSTALL.md.
Please refer to the libraries documentation for how to use the tactics.
Library developers can look at the comments in the theories/*.v files,
for instance starting with theories/checker.v.
Please report any bug / feature request in our issue tracker.
To be effective, bug reports should mention the OCaml version used
to compile and run Rocq, the Rocq version (rocq -v)
and include a complete source example leading to the bug.