aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/Psatz.v
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* micromega : more robust generation of proof termsGravatar Frédéric Besson2016-09-07
| | | | | | | - Assert a purely arihtmetic sub-goal that is proved independently by reflexion. (This reduces the stress on the conversion test) - Does not use 'abstract' anymore (more natural proof-term) - Fix a parsing bug (certain terms in Prop where not recognized)
* Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.Gravatar Frédéric Besson2016-08-31
| | | | If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
* plugin micromega : nra also handles non-linear rational arithmetic over Q ↵Gravatar Frédéric Besson2016-08-30
| | | | | | | (Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R.
* Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new ↵Gravatar Pierre Letouzey2016-05-19
| | | | Init/Tauto.v)
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
|
* 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
|
* micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)Gravatar Frédéric Besson2014-08-01
| | | | * Thanks to G. Melquiond for pointing out that 'abstract' already performs type-checking
* micromega : improve efficiency/termination of type-checkingGravatar Frédéric Besson2014-08-01
| | | | | * unused terms are generalised * proof is abstract
* micromega : refification recognises @eq T for T convertible with Z or RGravatar Frédéric Besson2014-07-31
|
* micromega: removal of spurious Export; addition of Lia.v encapsulating lia ↵Gravatar Frédéric Besson2013-12-20
| | | | and nia.
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Legacy Ring and Legacy Field migrated to contribsGravatar letouzey2012-07-05
| | | | | | | | | One slight point to check someday : fourier used to launch a tactic called Ring.polynom in some cases. It it crucial ? If so, how to replace with the setoid_ring equivalent ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
| | | | | | | | | | | | | | | | | | - For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
* update of Micromega docGravatar fbesson2011-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14248 85f007b7-540e-0410-9357-904b9bb8a0f7
* improved tactic namesGravatar fbesson2011-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14242 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 ↵Gravatar fbesson2011-05-23
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* added support to handle division by a constant over RGravatar fbesson2011-05-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14147 85f007b7-540e-0410-9357-904b9bb8a0f7
* cbv delta - [...] before calling liaGravatar fbesson2011-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14140 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
* Application des patches envoyés par F. Besson pour micromegaGravatar notin2010-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12852 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
* 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
* 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-06-29 16:42:00 +0000