aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
Commit message (Expand)AuthorAge
* 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
* Fixed bug #2036 (wrong copy-paste in RIneq) [copy of 11887 in branch v8.2]Gravatar herbelin2009-02-06
* Take advantage of natdynlink when available: almost all contribs become loada...Gravatar letouzey2008-12-16
* MAJ et bricoles diversesGravatar herbelin2008-05-12
* Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :Gravatar herbelin2008-04-06
* Suite 10760Gravatar herbelin2008-04-05
* - Retour en arrière sur la capacité du nouvel apply à utiliser lesGravatar herbelin2008-04-05
* - Amélioration de la présentation de RIneq, même si un nettoyage desGravatar herbelin2008-04-04
* Commit d'une preuve de l'axiome d'Archimède qui traînait dans mes placards.Gravatar herbelin2008-03-23
* Une passe sur les réels:Gravatar herbelin2008-03-23
* Marche-arrière sur la suppression de l'hypothèse inutile de Rpower_OGravatar herbelin2008-03-01
* Argumentation plus poussée de pourquoi on retire la condition x>0 dansGravatar herbelin2008-02-29
* Application patch #1807 sur hypothèse inutile de Rpower_OGravatar herbelin2008-02-27
* Essai de prise en compte de delta dans unify_0 (même sur termes non clos). Gravatar herbelin2008-02-13
* Nicer proofs.Gravatar roconnor2008-01-24
* remove Fourier Failure warnings.Gravatar roconnor2008-01-24