aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
Commit message (Expand)AuthorAge
* Remove fourier pluginGravatar Maxime Dénès2018-07-17
* Merge PR #6909: Deprecate Focus and UnfocusGravatar Maxime Dénès2018-03-08
|\
* \ Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \
| | * Remove all uses of Focus in standard library.Gravatar Théo Zimmermann2018-03-04
* | | Turn warning for deprecated notations on.Gravatar Théo Zimmermann2018-03-02
| |/ |/|
* | Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmasGravatar Maxime Dénès2018-02-28
|\ \
| | * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ |/|
| * weakens an hypothesis of Rle_RpowerGravatar Yves Bertot2017-09-06
| * changed statements of Rpower_lt and Rle_power and addedGravatar Yves Bertot2017-09-06
* | Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
|/
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove deprecated options from the standard library.Gravatar Guillaume Melquiond2017-06-14
* drop vo.itarget files and compute the corresponding the corresponding values ...Gravatar Matej Kosik2017-06-01
* Suppress warning message in stdlib.Gravatar Guillaume Melquiond2017-04-29
* Merge PR#414: Some more theory on powerRZ.Gravatar Maxime Dénès2017-04-27
|\
* | Add some hints to the "real" database to automatically discharge literal comp...Gravatar Guillaume Melquiond2017-04-07
* | Fix documentation typo (bug #5433).Gravatar Guillaume Melquiond2017-04-02
* | Simplify some proofs.Gravatar Guillaume Melquiond2017-04-02
* | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.Gravatar Guillaume Melquiond2017-03-30
* | Make IZR a morphism for field.Gravatar Guillaume Melquiond2017-03-22
* | Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
* | Make IZR use a compact representation of integers.Gravatar Guillaume Melquiond2017-03-22
* | Simplify some proofs using ring and field.Gravatar Guillaume Melquiond2017-03-22
| * Added some theory on powerRZ.Gravatar Thomas Sibut-Pinote2017-02-15
|/
* Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
* Fix an occurrence of deprecated eqn syntax in stdlib.Gravatar Maxime Dénès2016-08-18
* Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Revert "Temporary hack to compensate missing comma while re-printing tactic"Gravatar Hugo Herbelin2016-04-27
* Temporary hack to compensate missing comma while re-printing tacticGravatar Hugo Herbelin2016-04-27
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
* Accomodating #4166 (providing "Require Import OmegaTactic" as aGravatar Hugo Herbelin2015-04-01
* Add some missing Proof keywords.Gravatar Guillaume Melquiond2015-03-06
* Update headers.Gravatar Maxime Dénès2015-01-12
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* adds general facts in the Reals library, whose need was detected inGravatar Yves Bertot2014-09-23
* Change some Defined into Qed.Gravatar Guillaume Melquiond2014-09-17
* Add some missing Proof statements.Gravatar Guillaume Melquiond2014-09-17
* Change an axiom into a definition.Gravatar Guillaume Melquiond2014-09-17
* More proofs independent of the names generated by induction/elim overGravatar Hugo Herbelin2014-08-05
* Deactivate the "Standard Propositions Naming" flag, source of a lot ofGravatar Hugo Herbelin2014-06-26
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* Remove spurious Show in script.Gravatar Matthieu Sozeau2014-06-04
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Import proof of decidability of negated formulas from Coquelicot.Gravatar Guillaume Melquiond2014-04-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-30 19:25:06 +0000