aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
Commit message (Expand)AuthorAge
...
* 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
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* First release of Vector library.Gravatar pboutill2010-12-10
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
* Solve name conflict about pow introduced by commit 13546.Gravatar letouzey2010-10-21
* Numbers: new functions pow, even, odd + many reorganisationsGravatar letouzey2010-10-14
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Removed redundant and ill-named technical lemma.Gravatar gmelquio2010-02-18
* Removed SeqProp's dependency on Classical.Gravatar gmelquio2010-02-18
* Removed Rtrigo's dependency on Classical.Gravatar gmelquio2010-02-18
* Removed Rseries' dependency on Classical.Gravatar gmelquio2010-02-17
* Removed Rlimit's dependency on Classical.Gravatar gmelquio2010-02-17
* Removed Rderiv's dependency on Classical.Gravatar gmelquio2010-02-17
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
* Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni...Gravatar letouzey2010-01-07
* OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with...Gravatar letouzey2010-01-07
* Reverse order of arguments in min_case_strong for better uniformity (and comp...Gravatar letouzey2009-12-17
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* Fix anomaly when using typeclass resolution with filtered hyps in evars.Gravatar msozeau2009-12-06
* Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsGravatar letouzey2009-11-16
* DecidableType: A specification via boolean equality as an alternative to eq_decGravatar letouzey2009-11-10
* ROrderedType + Rminmax : Coq's Reals can be seen as OrderedType.Gravatar letouzey2009-11-03
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
* Added alternate versions of existing lemmas on sqrt.Gravatar gmelquio2009-11-02
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Removal of trailing spaces.Gravatar serpyc2009-10-04
* Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358.Gravatar herbelin2009-10-04
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Add a few properties about Rmin/Rmax with replication in Zmin/Zmax.Gravatar herbelin2009-09-27
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Added the following lemmas to homogenize Reals a bit:Gravatar gmelquio2009-09-11
* Parsing files for numerals (+ ascii/string) moved into pluginsGravatar letouzey2009-03-27
* - gros commit sur ring et field: passage des arguments simplifieGravatar barras2009-03-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 06:44:39 +0000