| Age | Commit message (Expand) | Author |
|---|
| 2019-04-02 | Add a Numeral Notation for QArith (e.g., 1.02e+01%Q for 102 # 10) | Pierre Roux |
| 2018-09-10 | Adapting standard library to the introduction of "Declare Scope". | Hugo Herbelin |
| 2018-03-09 | Merge PR #6155: Get rid of ' notation for Zpos in QArith | Maxime Dénès |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2017-11-14 | Get rid of ' notation for Zpos in QArith. | Robbert Krebbers |
| 2017-10-27 | Chaining two tactics in a proof | Raphaël Monat |
| 2017-10-25 | Moving from `is_true` to `= true` | Raphaël Monat |
| 2017-10-12 | Added proofs of Qeq_bool_refl, Qeq_bool_sym, Qeq_bool_trans. | Raphaël Monat |
| 2017-10-08 | Changed Qeq_bool_sym into Qeq_bool_comm, used the proof of @letouzey. | Raphaël Monat |
| 2017-10-03 | Add Qeq_bool_sym: Qeq_bool x y = Qeq_bool y x. | Raphaël Monat |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-05-02 | Eta contractions to please cbn | Pierre Boutillier |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2011-11-21 | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge |
| 2011-03-17 | CompareSpec: a slight generalization/reformulation of CompSpec | letouzey |
| 2010-11-02 | Add small utility lemmas about nat/P/Z/Q arithmetic. | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-29 | QArith: typo in name of hint db (fix #2346) | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-11-03 | Better visibility of the inductive CompSpec used to specify comparison functions | letouzey |
| 2009-11-03 | OrderedType implementation for various numerical datatypes + min/max structures | letouzey |
| 2009-10-08 | Implicit argument of Logic.eq become maximally inserted | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-08-05 | changed deprecated setoid into relation | amahboub |
| 2008-07-27 | Oups (on refait le 11268 en mieux) | herbelin |
| 2008-07-26 | - Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avec | herbelin |
| 2008-07-15 | Autour du parsing: | herbelin |
| 2008-07-04 | Fix bug #1899: no more strange notations for Qge and Qgt | letouzey |
| 2008-04-08 | - A little cleanup in Classes/*. Separate standard morphisms on | msozeau |
| 2008-03-16 | Reorganize Program and Classes theories. Requiring Setoid no longer sets | msozeau |
| 2008-03-06 | Plug the new setoid implemtation in, leaving the original one commented | msozeau |
| 2007-11-06 | small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is | letouzey |
| 2007-11-01 | Adding Qround.v (and helper lemmas and hints) | roconnor |
| 2007-09-07 | - renaming Qle_shift_recip_r into Qle_shift_inv_r, etc | roconnor |
| 2007-08-28 | Adding a few lemmas for reasoning about inequalities over the | roconnor |
| 2007-07-02 | Correction (partielle) du bug #1587 | notin |
| 2007-06-21 | Adding: Field instance for Q. | roconnor |
| 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 |
| 2006-09-21 | better scope/require managment (patch by Russel O'Connor) | letouzey |
| 2006-06-25 | nouvel algorithme pour Zgcd (plus rapide) + un Qcompare | letouzey |
| 2006-05-31 | ajout de QArith dans les theories standards | letouzey |
