aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith
Commit message (Expand)AuthorAge
* - Changement du code de Zplus pour accomoder ring qui sinon prend uneGravatar herbelin2008-05-11
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
* Correction du bug 1816 (ajout d'un lemme dans Znat) et suppressionGravatar notin2008-03-28
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* one more substitution s/Set/Type/Gravatar letouzey2008-03-04
* Proposal of a nice notation for constructors xI and xO of type positiveGravatar letouzey2008-02-10
* one forgotten compatibility lemmaGravatar letouzey2008-02-08
* Keep the Z_scope local to this file.Gravatar roconnor2008-01-24
* Adding Zdiv_le_compat_lGravatar thery2008-01-22
* A result about Zsgn(a/b), both for Zdiv and ZOdivGravatar letouzey2007-11-10
* First reasonably complete version of ZOdiv, including some propertiesGravatar letouzey2007-11-10
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10309 85f007b7-540e-0...Gravatar jforest2007-11-09
* more about ZOdiv and ZOmod (still not finished)Gravatar letouzey2007-11-09
* setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. Gravatar letouzey2007-11-08
* 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
* Adding Zdiv_mod_unique, Zdiv_opp_opp, Zdiv_mult_cancel, and Z_div_leGravatar roconnor2007-10-19
* Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.vGravatar emakarov2007-08-08
* A generic preprocessing tactic zify for (r)omegaGravatar letouzey2007-07-18
* normalisation (by closure) was not performed under fixpointsGravatar barras2007-07-12
* Transparency of Z_lt_le_decGravatar notin2007-04-12
* Bug nommage Zgt_trans_succGravatar herbelin2006-12-12
* correction Open Local Scope (Ring)Gravatar bgregoir2006-12-11
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* fixed field_simplify + changed precedence of let and fun in ltacGravatar barras2006-10-30
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
* Mise en forme des theoriesGravatar notin2006-10-17
* revert, the previous commit was a mistakeGravatar bertot2006-10-05
* A version of natprering that should be more efficient and removal of a badGravatar bertot2006-10-05
* Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynomGravatar barras2006-10-05
* commit de field + renommagesGravatar barras2006-09-26
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* Ajout de Zgcd_spec (compat.)Gravatar notin2006-06-26
* nouvel algorithme pour Zgcd (plus rapide) + un QcompareGravatar letouzey2006-06-25
* Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...Gravatar herbelin2006-06-09
* ajout de QArith dans les theories standardsGravatar letouzey2006-05-31
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
* Changement de précédence de l'argument du by de assert; conséquences...Gravatar herbelin2006-05-23
* On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_posGravatar letouzey2006-05-14
* typoGravatar letouzey2006-05-13
* un Zgcd calculant dans coqGravatar letouzey2006-05-13
* une fonction pouvant calculer le gcd en coqGravatar letouzey2006-05-11
* un Zgcd general gardant trace des coefsGravatar letouzey2006-05-05
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* Bug ScopeGravatar herbelin2006-02-12
* Nettoyage Zmin.v, création Zmax.v et Zminmax.vGravatar herbelin2006-02-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 23:28:12 +0000