aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
Commit message (Expand)AuthorAge
* 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
* Remove some uses of excluded middle.Gravatar Guillaume Melquiond2014-04-22
* Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Co...Gravatar Guillaume Melquiond2014-04-22
* Fixing missing headers.Gravatar Hugo Herbelin2014-04-16
* No more Coersion in Init.Gravatar Pierre Boutillier2014-04-10
* Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.Gravatar Guillaume Melquiond2014-03-10
* Add lemma derivable_pt_lim_atan.Gravatar Guillaume Melquiond2013-12-04
* Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Gravatar Guillaume Melquiond2013-12-03
* Remove a useless hypothesis from Rle_Rinv.Gravatar Guillaume Melquiond2013-12-03
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 19:50:27 +0000