| Age | Commit message (Expand) | Author |
|---|
| 2010-01-17 | BigN, BigZ, BigQ: presentation via unique module with both ops and props | letouzey |
| 2010-01-14 | Avoid some more re-declarations of Equivalence instances | letouzey |
| 2010-01-07 | Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders* | letouzey |
| 2010-01-07 | Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni... | letouzey |
| 2010-01-07 | OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with... | letouzey |
| 2009-12-09 | Factorisation between Makefile and ocamlbuild systems : .vo to compile are in... | letouzey |
| 2009-12-07 | No more specific syntax "Include Self" for inclusion of partially-applied fun... | letouzey |
| 2009-11-16 | Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxioms | letouzey |
| 2009-11-10 | DecidableType: A specification via boolean equality as an alternative to eq_dec | 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-11-02 | Remove various useless {struct} annotations | 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-10-03 | (Try to) use the conversion oracle also in w_unify to choose which constant to | msozeau |
| 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-24 | Tauto breaking not only binary "conjunctions" seems like a bad idea | msozeau |
| 2008-07-22 | A try at allowing matching on applications as a binary syntax node by default. | msozeau |
| 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-04-01 | Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient | herbelin |
| 2008-03-16 | Reorganize Program and Classes theories. Requiring Setoid no longer sets | msozeau |
| 2008-03-07 | Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part | msozeau |
| 2008-03-06 | Plug the new setoid implemtation in, leaving the original one commented | msozeau |
| 2008-02-05 | Add Morphisms for Qceiling and Qfloor | roconnor |
| 2007-11-24 | small improvements about Qc. Beware: Qlt_trans becomes Qclt_trans (as it ough... | letouzey |
| 2007-11-06 | small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is | letouzey |
| 2007-11-06 | Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of... | letouzey |
| 2007-11-01 | Adding Qround.v (and helper lemmas and hints) | roconnor |
| 2007-11-01 | In agreement with Laurent Thery, start migration of auxiliary results | letouzey |
| 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-13 | Added Qpower_plus' and Zpower_Qpower | roconnor |
| 2007-07-13 | Small cleanup | letouzey |
| 2007-07-05 | Added Qpower_mult theorem. | roconnor |
| 2007-07-02 | Correction (partielle) du bug #1587 | notin |
| 2007-06-25 | Updated Qpow_tac to work on a a more realistic set of exponent values. | roconnor |
| 2007-06-21 | Adding: Field instance for Q. | roconnor |
| 2006-12-11 | Changement dans le kernel : | bgregoir |
| 2006-10-17 | Mise en forme des theories | notin |
| 2006-09-29 | args implicites dans Field | barras |
| 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 |
| 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 |
