aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith
Commit message (Expand)AuthorAge
* Bug ScopeGravatar herbelin2006-02-12
* Nettoyage Zmin.v, création Zmax.v et Zminmax.vGravatar herbelin2006-02-12
* Finalement, préservation de la compatibilité pour Z_lt_induction et ajout p...Gravatar herbelin2005-05-02
* Lemme de passage de l'autre côté d'une égalitéGravatar herbelin2005-05-02
* Fixed hypotheses of Z_lt_induction (see #957)Gravatar herbelin2005-04-26
* Missing translating a 'O' into a '0' (again - cf bug #947); removed useless h...Gravatar herbelin2005-03-29
* Missing translating a 'O' into a '0'Gravatar herbelin2005-03-24
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* 'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...Gravatar herbelin2004-10-11
* Zbool déjà dans ZArith_baseGravatar herbelin2004-08-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* backtrack implicit dans BvectorGravatar marche2004-02-10
* patch Bvector: args implicitesGravatar marche2004-02-09
* changement de pose en set (pose n'etait pas utilise avec la semantiqueGravatar barras2003-12-24
* Duplication temporaire des règles de syntaxe des pairesGravatar herbelin2003-12-16
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
* Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...Gravatar herbelin2003-12-04
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* ground->firstorder, cc-> congruence, CC final commitGravatar corbinea2003-11-29
* Report de lemmes de Znumtheory dans Zabs ou BinIntGravatar herbelin2003-11-29
* Renoncement de la compatibilite des noms qualifies au profit de la compatibil...Gravatar herbelin2003-11-24
* CompatibiliteGravatar herbelin2003-11-22
* Simplification; ajout Zcompare_antisymGravatar herbelin2003-11-21
* ajout Pnat (suite)Gravatar herbelin2003-11-21
* ajout de Znumtheory.v dans ZArithGravatar letouzey2003-11-19
* Un nouveau lemme redondant ...Gravatar herbelin2003-11-18
* Deplacement ZERO_le_inj dans ZorderGravatar herbelin2003-11-18
* Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_baseGravatar herbelin2003-11-14
* cosmetiqueGravatar herbelin2003-11-14
* Quelques oublis pour que les notations marchent bienGravatar herbelin2003-11-14
* Bug implicit argumentsGravatar herbelin2003-11-14
* Oubli report Nul/PosGravatar herbelin2003-11-13
* RequireGravatar herbelin2003-11-13
* qq petit ajouts à ZdivGravatar letouzey2003-11-13
* Restructuration ZArithGravatar herbelin2003-11-12
* Ajout lemmes; independance vis a vis noms variables liees; restructurationGravatar herbelin2003-11-12
* Ajout partie sur bool anciennement dans ZmiscGravatar herbelin2003-11-12
* Ajout lemmes; independance vis a vis noms variables lieesGravatar herbelin2003-11-12
* Ajout quelques lemmes; noms des variables lieesGravatar herbelin2003-11-09
* Oubli BinNatGravatar herbelin2003-11-07
* Oubli d'un Set Implicit ArgumentsGravatar herbelin2003-11-07
* Des oublisGravatar herbelin2003-11-06
* Report des definitions sorties de fast_integer pour compatibiliteGravatar herbelin2003-11-06
* Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...Gravatar herbelin2003-11-05
* Exporting ^; utilisation arg scope impliciteGravatar herbelin2003-11-03
* Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...Gravatar herbelin2003-11-01
* Retour en arriere sur d'autres renommages de variablesGravatar herbelin2003-10-28
* Retour a un nommage non standard des variables pour compatibilite; report 're...Gravatar herbelin2003-10-27
* Documentation/StructurationGravatar herbelin2003-10-22
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22