aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/MExtraction.v
AgeCommit message (Expand)Author
2019-05-22Partly revert micromega parsing using typeclasses.Frédéric Besson
2019-04-01Several improvements and fixes of LiaFrédéric Besson
2018-10-09Refactoring of Micromega code using a Simplex linear solverFrédéric Besson
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-28Make the micromega extraction check a regular output test.Gaëtan Gilbert
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2017-06-14Makefile.build : cleanup now that micromega.ml isn't generated + sync check o...Pierre Letouzey
2017-06-12Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to ge...Matej Košík
2017-06-01Break circular dependency in MExtractionJason Gross
2017-06-01extract "plugins/micromega/micromega.ml{,i}" files from "plugins/micromega/ME...Matej Kosik
2016-09-07micromega : more robust generation of proof termsFrédéric Besson
2016-01-20Update copyright headers.Maxime Dénès
2015-04-02Fix some typos.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2012-08-08Updating headers.herbelin
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2011-05-20added support to handle division by a constant over Rfbesson
2011-05-09Improved lia + experimental nliafbesson
2010-07-24Updated all headers for 8.3 and trunkherbelin
2009-09-18micromega: better handling of exponentiation + correction of test-suite termi...fbesson
2009-07-30micromega : Better parsing of formulae - smaller proof terms for Z - redesign...fbesson
2009-03-29Micromega: improvement of the code obtained by extractionletouzey
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:15:46 +0000