aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
Commit message (Expand)AuthorAge
* 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
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Removing redundant definition of case_eq (see #2919).Gravatar herbelin2012-10-16
* Updating headers.Gravatar herbelin2012-08-08
* Legacy Ring and Legacy Field migrated to contribsGravatar letouzey2012-07-05
* Some cleanup in recent proofs concerning piGravatar letouzey2012-07-05
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* These files are displaced from Rtrigo.v and Ranalysis_reg.vGravatar bertot2012-06-11
* finish the rearrangement for removing the sin_PI2 axiom. This new versionGravatar bertot2012-06-11
* Adds the proof of PI_ineq, plus some other smarter ways to approximate PIGravatar bertot2012-06-11
* Modifications and rearrangements to remove the action that sin (PI/2) = 1Gravatar bertot2012-06-05
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Cleaning a little bit the files talking about descriptions: avoidingGravatar herbelin2011-11-03
* BinInt: Z.add become the alternative Z.add'Gravatar letouzey2011-05-05
* - Improve unification (beta-reduction, and same heuristic as evarconv for red...Gravatar msozeau2011-04-13
* Fix scripts relying on unification not doing any beta reduction.Gravatar msozeau2011-04-13
* Unify meta types with the right flags, add betaiotazeta reduction to unificat...Gravatar msozeau2011-04-13
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 13:20:43 +0000