aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/Lra.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.