aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
Commit message (Expand)AuthorAge
* 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
* Prove the decidability of arithmetical statements using the real numbers.Gravatar roconnor2008-01-24
* Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0Gravatar herbelin2007-09-27
* Changement dans ring et field, beaucoup de correction d'erreurs,Gravatar bgregoir2006-12-15
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* fixed field_simplify + changed precedence of let and fun in ltacGravatar barras2006-10-30
* LegacyRfield was opening R_scopeGravatar barras2006-10-30
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
* Le caractère ² fait planter make docGravatar notin2006-10-27
* Mise en forme des theoriesGravatar notin2006-10-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 01:08:08 +0000