| Age | Commit message (Expand) | Author |
|---|
| 2011-11-21 | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge |
| 2011-08-17 | Smaller proof terms for QcPower_{0,pos} | glondu |
| 2011-06-24 | Clean-up of Znumtheory, deletion of Zgcd_def | letouzey |
| 2011-05-05 | BinInt: Z.add become the alternative Z.add' | letouzey |
| 2011-05-05 | Modularization of BinPos + fixes in Stdlib | letouzey |
| 2011-03-17 | CompareSpec: a slight generalization/reformulation of CompSpec | letouzey |
| 2010-12-10 | First release of Vector library. | pboutill |
| 2010-11-05 | Numbers: axiomatization, properties and implementations of gcd | 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 |
| 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 |
