aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith
AgeCommit message (Expand)Author
2006-05-14On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_posletouzey
2006-05-13typoletouzey
2006-05-13un Zgcd calculant dans coqletouzey
2006-05-11une fonction pouvant calculer le gcd en coqletouzey
2006-05-05un Zgcd general gardant trace des coefsletouzey
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...notin
2006-02-12Bug Scopeherbelin
2006-02-12Nettoyage Zmin.v, création Zmax.v et Zminmax.vherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 08:50:20 +0000