| Age | Commit message (Expand) | Author |
|---|
| 2020-11-16 | Explicitly annotate all hint declarations of the standard library. | Pierre-Marie Pédrot |
| 2020-03-18 | Update headers in the whole code base. | Théo Zimmermann |
| 2019-12-17 | [micromega] fix efficiency regression | Frédéric Besson |
| 2019-10-28 | [stdlib]Reals: use “lia” rather than “omega” | Vincent Laporte |
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 2017-04-29 | Suppress warning message in stdlib. | Guillaume Melquiond |
| 2017-04-27 | Merge PR#414: Some more theory on powerRZ. | Maxime Dénès |
| 2017-03-22 | Change the parser and printer so that they use IZR for real constants. | Guillaume Melquiond |
| 2017-02-15 | Added some theory on powerRZ. | Thomas Sibut-Pinote |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-09-23 | adds general facts in the Reals library, whose need was detected in | Yves Bertot |
| 2014-06-04 | Remove spurious Show in script. | Matthieu Sozeau |
| 2014-06-01 | Making those proofs which depend on names generated for the arguments | Hugo Herbelin |
| 2012-10-16 | Removing redundant definition of case_eq (see #2919). | herbelin |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-05 | Open Local Scope ---> Local Open Scope, same with Notation and alii | letouzey |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2012-06-05 | Modifications and rearrangements to remove the action that sin (PI/2) = 1 | bertot |
| 2011-05-05 | BinInt: Z.add become the alternative Z.add' | letouzey |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2010-11-18 | Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-11-02 | Remove various useless {struct} annotations | letouzey |
| 2009-10-08 | Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False' | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-11 | Added the following lemmas to homogenize Reals a bit: | gmelquio |
| 2008-04-06 | Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt : | herbelin |
| 2008-04-05 | Suite 10760 | herbelin |
| 2008-03-23 | Une passe sur les réels: | herbelin |
| 2006-12-15 | Changement dans ring et field, beaucoup de correction d'erreurs, | bgregoir |
| 2006-12-11 | Changement dans le kernel : | bgregoir |
| 2006-10-27 | simplif de la partie ML de ring/field | barras |
| 2006-10-17 | Mise en forme des theories | notin |
| 2006-09-26 | commit de field + renommages | barras |
| 2006-09-26 | mise a jour du nouveau ring et ajout du nouveau field, avant renommages | barras |
| 2004-11-22 | compatibility with POWERPC | gregoire |
| 2004-11-12 | Changement dans les boxed values . | gregoire |
| 2004-10-20 | COMMITED BYTECODE COMPILER | barras |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-03-12 | ajout decimal_exp pour interpreter les notations decimales | mohring |
| 2003-12-15 | modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes | barras |
| 2003-12-05 | power associe a droite | marche |
| 2003-11-29 | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin |
| 2003-11-02 | Restauration preference Rge a Rle pour compatibilite... | herbelin |
| 2003-10-13 | Notations pour l'exponentiation | herbelin |
| 2003-10-10 | Notation '^' | herbelin |
