| Age | Commit message (Expand) | Author |
|---|
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 2017-04-07 | Add some hints to the "real" database to automatically discharge literal comp... | Guillaume Melquiond |
| 2017-04-02 | Simplify some proofs. | Guillaume Melquiond |
| 2017-03-30 | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R. | Guillaume Melquiond |
| 2017-03-22 | Make IZR a morphism for field. | Guillaume Melquiond |
| 2017-03-22 | Change the parser and printer so that they use IZR for real constants. | Guillaume Melquiond |
| 2017-03-22 | Make IZR use a compact representation of integers. | Guillaume Melquiond |
| 2017-03-22 | Simplify some proofs using ring and field. | Guillaume Melquiond |
| 2016-10-24 | Remove v62 from stdlib. | Théo Zimmermann |
| 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-01 | Making those proofs which depend on names generated for the arguments | Hugo Herbelin |
| 2014-05-06 | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | Matthieu Sozeau |
| 2014-03-10 | Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r. | Guillaume Melquiond |
| 2013-12-03 | Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l. | Guillaume Melquiond |
| 2013-12-03 | Remove a useless hypothesis from Rle_Rinv. | Guillaume Melquiond |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-05 | Kills the useless tactic annotations "in |- *" | 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 |
| 2012-04-15 | Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680). | herbelin |
| 2011-05-05 | BinInt: Z.add become the alternative Z.add' | 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-10-08 | Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False' | letouzey |
| 2009-09-28 | Fix the stdlib doc compilation + switch all .v file to utf8 | 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 |
| 2009-03-17 | - gros commit sur ring et field: passage des arguments simplifie | barras |
| 2009-02-06 | Fixed bug #2036 (wrong copy-paste in RIneq) [copy of 11887 in branch v8.2] | herbelin |
| 2008-04-06 | Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt : | herbelin |
| 2008-04-05 | - Retour en arrière sur la capacité du nouvel apply à utiliser les | herbelin |
| 2008-04-04 | - Amélioration de la présentation de RIneq, même si un nettoyage des | 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-10-27 | simplif de la partie ML de ring/field | barras |
| 2006-10-17 | Mise en forme des theories | notin |
| 2006-09-28 | separation de RealField | barras |
| 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 |
| 2005-03-29 | Missing translating a 'O' into a '0' (again) | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-12-15 | modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes | barras |
| 2003-12-01 | Ratage standardisation Rge_monotony en Rmult_ge_compat_r | herbelin |
| 2003-11-29 | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin |
| 2003-11-29 | Ajout lemmes, simplification preuve de SeqProp | herbelin |
| 2003-11-28 | Protection contre les renommages; redondances | herbelin |
