aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
...
* 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
* Oubli BinNatGravatar herbelin2003-11-07
* Oubli d'un Set Implicit ArgumentsGravatar herbelin2003-11-07
* Biblio standard sans mention de la possibilite d'etre impredicatifGravatar herbelin2003-11-07
* Biblio standard sans impredicativiteGravatar herbelin2003-11-07
* Des oublisGravatar herbelin2003-11-06
* Report des definitions sorties de fast_integer pour compatibiliteGravatar herbelin2003-11-06
* NotationsGravatar herbelin2003-11-05
* Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...Gravatar herbelin2003-11-05
* Preuve de l'incoherence de {A}+{~A} avec Set impredicatifGravatar herbelin2003-11-05
* RedondancesGravatar herbelin2003-11-05
* 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
* CosmetiqueGravatar herbelin2003-11-02
* Renforcement significatif du resultat principalGravatar herbelin2003-11-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 12:21:35 +0000