| Commit message (Expand) | Author | Age |
|---|
| * | Smaller proof terms for QcPower_{0,pos} |  glondu | 2011-08-17 |
| * | Clean-up of Znumtheory, deletion of Zgcd_def |  letouzey | 2011-06-24 |
| * | BinInt: Z.add become the alternative Z.add' | letouzey | 2011-05-05 |
| * | Modularization of BinPos + fixes in Stdlib | letouzey | 2011-05-05 |
| * | CompareSpec: a slight generalization/reformulation of CompSpec | letouzey | 2011-03-17 |
| * | First release of Vector library. |  pboutill | 2010-12-10 |
| * | Numbers: axiomatization, properties and implementations of gcd | letouzey | 2010-11-05 |
| * | Add small utility lemmas about nat/P/Z/Q arithmetic. | letouzey | 2010-11-02 |
| * | Updated all headers for 8.3 and trunk |  herbelin | 2010-07-24 |
| * | QArith: typo in name of hint db (fix #2346) | letouzey | 2010-06-29 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | BigN, BigZ, BigQ: presentation via unique module with both ops and props | letouzey | 2010-01-17 |
| * | Avoid some more re-declarations of Equivalence instances | letouzey | 2010-01-14 |
| * | 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 | 2010-01-07 |
| * | Factorisation between Makefile and ocamlbuild systems : .vo to compile are in... | letouzey | 2009-12-09 |
| * | No more specific syntax "Include Self" for inclusion of partially-applied fun... | letouzey | 2009-12-07 |
| * | Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxioms | letouzey | 2009-11-16 |
| * | DecidableType: A specification via boolean equality as an alternative to eq_dec | letouzey | 2009-11-10 |
| * | 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-03 |
| * | Remove various useless {struct} annotations | letouzey | 2009-11-02 |
| * | Implicit argument of Logic.eq become maximally inserted | letouzey | 2009-10-08 |
| * | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
| * | changed deprecated setoid into relation |  amahboub | 2009-08-05 |
| * | (Try to) use the conversion oracle also in w_unify to choose which constant to |  msozeau | 2008-10-03 |
| * | Oups (on refait le 11268 en mieux) | herbelin | 2008-07-27 |
| * | - Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avec | herbelin | 2008-07-26 |
| * | Tauto breaking not only binary "conjunctions" seems like a bad idea | msozeau | 2008-07-24 |
| * | A try at allowing matching on applications as a binary syntax node by default. | msozeau | 2008-07-22 |
| * | Autour du parsing: | herbelin | 2008-07-15 |
| * | Fix bug #1899: no more strange notations for Qge and Qgt | letouzey | 2008-07-04 |
| * | - A little cleanup in Classes/*. Separate standard morphisms on | msozeau | 2008-04-08 |
| * | Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient | herbelin | 2008-04-01 |
| * | Reorganize Program and Classes theories. Requiring Setoid no longer sets | msozeau | 2008-03-16 |
| * | Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part | msozeau | 2008-03-07 |
| * | Plug the new setoid implemtation in, leaving the original one commented | msozeau | 2008-03-06 |
| * | Add Morphisms for Qceiling and Qfloor |  roconnor | 2008-02-05 |
| * | small improvements about Qc. Beware: Qlt_trans becomes Qclt_trans (as it ough... | letouzey | 2007-11-24 |
| * | 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-06 |
| * | Adding Qround.v (and helper lemmas and hints) | roconnor | 2007-11-01 |
| * | In agreement with Laurent Thery, start migration of auxiliary results | letouzey | 2007-11-01 |
| * | - renaming Qle_shift_recip_r into Qle_shift_inv_r, etc | roconnor | 2007-09-07 |
| * | Adding a few lemmas for reasoning about inequalities over the | roconnor | 2007-08-28 |
| * | Added Qpower_plus' and Zpower_Qpower | roconnor | 2007-07-13 |
| * | Small cleanup | letouzey | 2007-07-13 |
| * | Added Qpower_mult theorem. | roconnor | 2007-07-05 |
| * | Correction (partielle) du bug #1587 |  notin | 2007-07-02 |
glondu
letouzey
pboutill
herbelin
amahboub
msozeau
roconnor
notin