aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/coq_micromega.ml
AgeCommit message (Expand)Author
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-06-01More cleaningppedrot
2012-04-12lib directory is cut in 2 cma.pboutill
2012-01-14coq_micromega.ml: fix order of recursive calls to rconstantglondu
2012-01-14More newlines in debugging output of psatzlglondu
2011-07-29Coq_micromega: generic = on constr replaced by eq_constrpuech
2011-05-25Q2R -> IQRfbesson
2011-05-23git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0...fbesson
2011-05-20added support to handle division by a constant over Rfbesson
2011-05-18apply zeta reduction before syntaxificationfbesson
2011-05-09Improved lia + experimental nliafbesson
2011-05-05Definitions of positive, N, Z moved in Numbers/BinNums.vletouzey
2010-10-21Solve name conflict about pow introduced by commit 13546.letouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-28Modify the test for csdp and associated message.fkirchne
2010-05-28...fkirchne
2010-04-11Look for csdp in $PATH at runtime, remove -csdpdir configure optionglondu
2010-03-08Application des patches envoyés par F. Besson pour micromeganotin
2009-11-03OrderedType implementation for various numerical datatypes + min/max structuresletouzey
2009-10-04Removal of trailing spaces.serpyc
2009-09-18micromega: better handling of exponentiation + correction of test-suite termi...fbesson
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-25git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0...fbesson
2009-08-20new csdp cache + improved error messagefbesson
2009-08-20new csdp cache + improved error messagefbesson
2009-07-31addition of lia.cache - csdp.cache is now handled by micromega not csdpcertfbesson
2009-07-30micromega : Better parsing of formulae - smaller proof terms for Z - redesign...fbesson
2009-05-11micromega: proof compression bugfixfbesson
2009-03-29Micromega: improvement of the code obtained by extractionletouzey
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey