aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/mutils.ml
Commit message (Collapse)AuthorAge
* Micromega clean-upGravatar Maxime Dénès2018-06-07
| | | | | | | | | We add .mli files, removed dead code and use standard combinators instead of redefined ad-hoc ones in a few places. A lot of cleaning still has to be done on this code: documenting the interfaces, resolving the many abstraction leaks. I suspect there is still a lot of code duplication.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Fix Bug #5073 : regression of micromega pluginGravatar Frédéric Besson2016-09-08
| | | | | The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm) instead of apply (__arith P1 ... Pn) which unification could fail.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | maintenance micromega pluginGravatar Frédéric Besson2015-04-28
|/ | | | | | - add a nra tactic (similar to nia) for non-linear real arithmetic tactic - fix a long-standing bug in the reification code - port to the new proof-engine
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Fixing some generic equalities in Micromega.Gravatar Pierre-Marie Pédrot2014-03-03
|
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
|
* Relaunch all Unix.waitpid when they ended with EINTRGravatar Pierre Letouzey2014-01-30
| | | | Moreover, cleanup of System.connect (used by the "external" tactic).
* Restrict (try...with...) to avoid catching critical exn (part 15)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16292 85f007b7-540e-0410-9357-904b9bb8a0f7
* invalid_arg instead of raise (Invalid_argement ...)Gravatar letouzey2013-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16270 85f007b7-540e-0410-9357-904b9bb8a0f7
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved lia + experimental nliaGravatar fbesson2011-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14116 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* A little bit of cleanup, and some annotations.Gravatar fkirchne2010-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13036 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 ↵Gravatar fbesson2009-08-25
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* new csdp cache + improved error messageGravatar fbesson2009-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12287 85f007b7-540e-0410-9357-904b9bb8a0f7
* new csdp cache + improved error messageGravatar fbesson2009-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12286 85f007b7-540e-0410-9357-904b9bb8a0f7
* micromega : Better parsing of formulae - smaller proof terms for Z - ↵Gravatar fbesson2009-07-30
| | | | | | redesign of proof cache git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12254 85f007b7-540e-0410-9357-904b9bb8a0f7
* Micromega: improvement of the code obtained by extractionGravatar letouzey2009-03-29
| | | | | | | | | | | | | | | | | * In eval_cone and simpl_cone, default patterns were leading to duplicated computations. Adaptation of RingMicromega.v to prevent that. * Use the Ocaml builtin types (lists, pairs, bool, etc) and remove the useless conversion functions in mutils.ml and alii. * andb was extracted to a correctly lazy but ugly match. Let's rather use Ocaml's (&&). Remain to be done: take advantage of extraction during the build, - either directly if we are using plugins, (no dependency issues) - or if we compile statically, at least check later that the micromega.ml in the archive and the one auto-generated are in sync. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12034 85f007b7-540e-0410-9357-904b9bb8a0f7
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵Gravatar letouzey2009-03-20
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 22:55:11 +0000