aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Ratage standardisation Rge_monotony en Rmult_ge_compat_rGravatar herbelin2003-12-01
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Notation locale pour RpowerGravatar herbelin2003-11-29
* Ajout lemmes, simplification preuve de SeqPropGravatar herbelin2003-11-29
* ground->firstorder, cc-> congruence, CC final commitGravatar corbinea2003-11-29
* Utilisation du total_order non constructifGravatar herbelin2003-11-29
* Report de lemmes de Znumtheory dans Zabs ou BinIntGravatar herbelin2003-11-29
* Protection contre les renommages; redondancesGravatar herbelin2003-11-28
* 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 Pnat (suite)Gravatar herbelin2003-11-21
* Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase e...Gravatar herbelin2003-11-21
* Tri et typoGravatar herbelin2003-11-21
* ajout de Znumtheory.v dans ZArithGravatar letouzey2003-11-19
* Restauration compatibilite 7.4 pour le Hint Unfold RgtGravatar herbelin2003-11-19
* Un nouveau lemme redondant ...Gravatar herbelin2003-11-18
* Deplacement ZERO_le_inj dans ZorderGravatar herbelin2003-11-18
* Meilleure solution pour la compatibiliteGravatar herbelin2003-11-15
* Pour les .v8Gravatar herbelin2003-11-14
* Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_baseGravatar herbelin2003-11-14
* cosmetiqueGravatar herbelin2003-11-14
* PresentationGravatar herbelin2003-11-14
* Ordre standard pour l'associativiteGravatar herbelin2003-11-14
* Quelques oublis pour que les notations marchent bienGravatar herbelin2003-11-14
* Bug implicit argumentsGravatar herbelin2003-11-14
* Automatisation de la traduction de iff_trans; renommage IFGravatar herbelin2003-11-14
* Backtrack sur PeanoGravatar herbelin2003-11-14
* Nouveaux lemmes 'canoniques'; compatibiliteGravatar herbelin2003-11-14
* moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...Gravatar barras2003-11-13
* Oubli report Nul/PosGravatar herbelin2003-11-13
* RequireGravatar herbelin2003-11-13
* qq petit ajouts à ZdivGravatar letouzey2003-11-13
* MAJ INZGravatar herbelin2003-11-12
* Ajout lemme projectionsGravatar herbelin2003-11-12
* %type au lieu de %TGravatar herbelin2003-11-12
* Lemmes dans un sens plus naturelGravatar herbelin2003-11-12
* Restructuration ZArithGravatar herbelin2003-11-12
* CosmetiqueGravatar herbelin2003-11-12
* Noms canoniques pour les variables lieesGravatar herbelin2003-11-12
* Independance vis a vis noms variables liees; partie sur bool dans ZboolGravatar herbelin2003-11-12
* Noms/énoncés plus canoniquesGravatar herbelin2003-11-12
* Independance vis a vis noms variables lieesGravatar 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
* On sait jamaisGravatar herbelin2003-11-12
* petits changements de syntaxeGravatar barras2003-11-12
* Ajout quelques lemmes; noms des variables lieesGravatar herbelin2003-11-09