aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith
AgeCommit message (Expand)Author
2005-05-02Finalement, préservation de la compatibilité pour Z_lt_induction et ajout p...herbelin
2005-05-02Lemme de passage de l'autre côté d'une égalitéherbelin
2005-04-26Fixed hypotheses of Z_lt_induction (see #957)herbelin
2005-03-29Missing translating a 'O' into a '0' (again - cf bug #947); removed useless h...herbelin
2005-03-24Missing translating a 'O' into a '0'herbelin
2004-11-12Changement dans les boxed values .gregoire
2004-10-11'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...herbelin
2004-08-03Zbool déjà dans ZArith_baseherbelin
2004-07-16Nouvelle en-têteherbelin
2004-02-10backtrack implicit dans Bvectormarche
2004-02-09patch Bvector: args implicitesmarche
2003-12-24changement de pose en set (pose n'etait pas utilise avec la semantiquebarras
2003-12-16Duplication temporaire des règles de syntaxe des pairesherbelin
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
2003-12-04Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...herbelin
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
2003-11-29Report de lemmes de Znumtheory dans Zabs ou BinIntherbelin
2003-11-24Renoncement de la compatibilite des noms qualifies au profit de la compatibil...herbelin
2003-11-22Compatibiliteherbelin
2003-11-21Simplification; ajout Zcompare_antisymherbelin
2003-11-21ajout Pnat (suite)herbelin
2003-11-19ajout de Znumtheory.v dans ZArithletouzey
2003-11-18Un nouveau lemme redondant ...herbelin
2003-11-18Deplacement ZERO_le_inj dans Zorderherbelin
2003-11-14Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_baseherbelin
2003-11-14cosmetiqueherbelin
2003-11-14Quelques oublis pour que les notations marchent bienherbelin
2003-11-14Bug implicit argumentsherbelin
2003-11-13Oubli report Nul/Posherbelin
2003-11-13Requireherbelin
2003-11-13qq petit ajouts à Zdivletouzey
2003-11-12Restructuration ZArithherbelin
2003-11-12Ajout lemmes; independance vis a vis noms variables liees; restructurationherbelin
2003-11-12Ajout partie sur bool anciennement dans Zmischerbelin
2003-11-12Ajout lemmes; independance vis a vis noms variables lieesherbelin
2003-11-09Ajout quelques lemmes; noms des variables lieesherbelin
2003-11-07Oubli BinNatherbelin
2003-11-07Oubli d'un Set Implicit Argumentsherbelin
2003-11-06Des oublisherbelin
2003-11-06Report des definitions sorties de fast_integer pour compatibiliteherbelin
2003-11-05Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...herbelin
2003-11-03Exporting ^; utilisation arg scope impliciteherbelin
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...herbelin
2003-10-28Retour en arriere sur d'autres renommages de variablesherbelin
2003-10-27Retour a un nommage non standard des variables pour compatibilite; report 're...herbelin
2003-10-22Documentation/Structurationherbelin
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
2003-10-21Redondance de dec_eq_natherbelin
2003-10-21Type relation dans Datatypesherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:45:43 +0000