aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/QArith
Commit message (Expand)AuthorAge
* - A little cleanup in Classes/*. Separate standard morphisms onGravatar msozeau2008-04-08
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Reorganize Program and Classes theories. Requiring Setoid no longer setsGravatar msozeau2008-03-16
* Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partGravatar msozeau2008-03-07
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* Add Morphisms for Qceiling and QfloorGravatar roconnor2008-02-05
* small improvements about Qc. Beware: Qlt_trans becomes Qclt_trans (as it ough...Gravatar letouzey2007-11-24
* small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is Gravatar letouzey2007-11-06
* Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...Gravatar letouzey2007-11-06
* Adding Qround.v (and helper lemmas and hints)Gravatar roconnor2007-11-01
* In agreement with Laurent Thery, start migration of auxiliary results Gravatar letouzey2007-11-01
* - renaming Qle_shift_recip_r into Qle_shift_inv_r, etcGravatar roconnor2007-09-07
* Adding a few lemmas for reasoning about inequalities over the Gravatar roconnor2007-08-28
* Added Qpower_plus' and Zpower_QpowerGravatar roconnor2007-07-13
* Small cleanupGravatar letouzey2007-07-13
* Added Qpower_mult theorem.Gravatar roconnor2007-07-05
* Correction (partielle) du bug #1587Gravatar notin2007-07-02
* Updated Qpow_tac to work on a a more realistic set of exponent values.Gravatar roconnor2007-06-25
* Adding: Field instance for Q.Gravatar roconnor2007-06-21
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* Mise en forme des theoriesGravatar notin2006-10-17
* args implicites dans FieldGravatar barras2006-09-29
* separation de RealFieldGravatar barras2006-09-28
* commit de field + renommagesGravatar barras2006-09-26
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* better scope/require managment (patch by Russel O'Connor)Gravatar letouzey2006-09-21
* nouvel algorithme pour Zgcd (plus rapide) + un QcompareGravatar letouzey2006-06-25
* ajout de QArith dans les theories standardsGravatar letouzey2006-05-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 23:26:53 +0000