aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2004-01-13Suppression de Rsyntax en v8herbelin
2004-01-09bugs avec Pose et Assertbarras
2004-01-09Commentaires en v8herbelin
2003-12-24Ajout delimiteur et arguments de scope pour listherbelin
2003-12-24changement de pose en set (pose n'etait pas utilise avec la semantiquebarras
2003-12-23Finalement, espacement autour du ':' pour a la fois exists, forall et funherbelin
2003-12-21Affichage sur le modèle du forall pour le existsherbelin
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-05power associe a droitemarche
2003-12-04Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...herbelin
2003-12-01Ratage standardisation Rge_monotony en Rmult_ge_compat_rherbelin
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-29Notation locale pour Rpowerherbelin
2003-11-29Ajout lemmes, simplification preuve de SeqPropherbelin
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
2003-11-29Utilisation du total_order non constructifherbelin
2003-11-29Report de lemmes de Znumtheory dans Zabs ou BinIntherbelin
2003-11-28Protection contre les renommages; redondancesherbelin
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-21ajout Pnat (suite)herbelin
2003-11-21Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase e...herbelin
2003-11-21Tri et typoherbelin
2003-11-19ajout de Znumtheory.v dans ZArithletouzey
2003-11-19Restauration compatibilite 7.4 pour le Hint Unfold Rgtherbelin
2003-11-18Un nouveau lemme redondant ...herbelin
2003-11-18Deplacement ZERO_le_inj dans Zorderherbelin
2003-11-15Meilleure solution pour la compatibiliteherbelin
2003-11-14Pour les .v8herbelin
2003-11-14Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_baseherbelin
2003-11-14cosmetiqueherbelin
2003-11-14Presentationherbelin
2003-11-14Ordre standard pour l'associativiteherbelin
2003-11-14Quelques oublis pour que les notations marchent bienherbelin
2003-11-14Bug implicit argumentsherbelin
2003-11-14Automatisation de la traduction de iff_trans; renommage IFherbelin
2003-11-14Backtrack sur Peanoherbelin
2003-11-14Nouveaux lemmes 'canoniques'; compatibiliteherbelin
2003-11-13moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...barras
2003-11-13Oubli report Nul/Posherbelin
2003-11-13Requireherbelin
2003-11-13qq petit ajouts à Zdivletouzey
2003-11-12MAJ INZherbelin
2003-11-12Ajout lemme projectionsherbelin
2003-11-12%type au lieu de %Therbelin
2003-11-12Lemmes dans un sens plus naturelherbelin
2003-11-12Restructuration ZArithherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 00:27:44 +0000