aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rfunctions.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* 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
|\
* | Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
| * Added some theory on powerRZ.Gravatar Thomas Sibut-Pinote2017-02-15
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* adds general facts in the Reals library, whose need was detected inGravatar Yves Bertot2014-09-23
* 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
* Removing redundant definition of case_eq (see #2919).Gravatar herbelin2012-10-16
* Updating headers.Gravatar herbelin2012-08-08
* 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
* Modifications and rearrangements to remove the action that sin (PI/2) = 1Gravatar bertot2012-06-05
* BinInt: Z.add become the alternative Z.add'Gravatar letouzey2011-05-05
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Added the following lemmas to homogenize Reals a bit:Gravatar gmelquio2009-09-11
* Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :Gravatar herbelin2008-04-06
* Suite 10760Gravatar herbelin2008-04-05
* Une passe sur les réels:Gravatar herbelin2008-03-23
* Changement dans ring et field, beaucoup de correction d'erreurs,Gravatar bgregoir2006-12-15
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
* Mise en forme des theoriesGravatar notin2006-10-17
* commit de field + renommagesGravatar barras2006-09-26
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* compatibility with POWERPCGravatar gregoire2004-11-22
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* ajout decimal_exp pour interpreter les notations decimalesGravatar mohring2004-03-12
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
* power associe a droiteGravatar marche2003-12-05
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Restauration preference Rge a Rle pour compatibilite...Gravatar herbelin2003-11-02
* Notations pour l'exponentiationGravatar herbelin2003-10-13
* Notation '^'Gravatar herbelin2003-10-10
* Ajout et MAJ commandes de scopesGravatar herbelin2003-09-12
* BugGravatar herbelin2003-05-21
* Amelioration presentationGravatar herbelin2003-05-14
* Amelioration affichageGravatar herbelin2003-05-14
* Deplacement lemmes sur fact de Reals vers ArithGravatar herbelin2003-05-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-21 23:35:38 +0000