aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum/micromega.rst
AgeCommit message (Expand)Author
2021-04-16[zify] bugfixFrederic Besson
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-01-25Update doc/sphinx/addendum/micromega.rstFrédéric Besson
2021-01-22[micromega] Deprecate hopefully useless options and flagsBESSON Frederic
2021-01-19Remove Add InjTyp and 10 other micromega commandsJim Fehrle
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
2020-11-05Change the title of the automatic tactic chapter and of its sections.Théo Zimmermann
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-22Merge PR #11924: Add style for smallcaps.coqbot-app[bot]
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-10-20[zify] Use flag for Z.to_euclidean_division_equations.Frédéric Besson
2020-10-20[zify] Add support for Int63.intFrédéric Besson
2020-09-11Minimal changes to make the refman compatible with Sphinx 3.Théo Zimmermann
2020-09-03Merge PR #12953: Add :math: around mathcoqbot-app[bot]
2020-08-30Add :math: around mathJason Gross
2020-08-30Fix rendering of -> in micromegaJason Gross
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-14Update zify documentationFrédéric Besson
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
2020-04-17Deprecate “omega”Vincent Laporte
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-03Fix efficiency regression #11436Frédéric Besson
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-10-03Improved handling of micromega cachesFrédéric Besson
2019-09-16Re-implementation of zifyFrédéric Besson
2019-02-12Fix failing coqtops in micromega.rst (the main one requires csdp)Gaëtan Gilbert
2019-01-24Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, Z.to_euclidean_div...Jason Gross
2019-01-24Revert "Add subst to the end of nia in the test-suite"Jason Gross
2019-01-24Add subst to the end of nia in the test-suiteJason Gross
2019-01-24Don't bundle Z.div_mod_quot_rem into zifyJason Gross
2019-01-24Add Z.div_mod_to_quot_rem tactic, put it in zifyJason Gross
2019-01-22Remove unneeded | in productionlistsJim Fehrle
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try t...Théo Zimmermann
2018-11-19Minor update to micromega.rstsoraros
2018-10-09Refactoring of Micromega code using a Simplex linear solverFrédéric Besson
2018-09-25Remove romegaVincent Laporte
2018-08-01Improved grammar and spelling in chapters 'Type Classes', 'Omega' and 'Microm...Zeimer
2018-07-17Remove fourier pluginMaxime Dénès
2018-05-15[doc] Small fixesClément Pit-Claudel
2018-05-05[sphinx] Fix some references.Théo Zimmermann
2018-04-16[Sphinx] Clean-up indicesMaxime Dénès
2018-03-22[Sphinx] Add chapter 22Maxime Dénès
2018-03-22[Sphinx] Move chapter 22 to new infrastructureMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:13:36 +0000