aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2004-03-29Commentairesherbelin
2004-03-28Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...herbelin
2004-03-24MAJ commentairesherbelin
2004-03-17Definition de la notation de la paire par un motif recursifherbelin
2004-03-17Commentairesherbelin
2004-03-12ajout decimal_exp pour interpreter les notations decimalesmohring
2004-03-03ide: silent behavior better, save icon, -byte worksmarche
2004-02-28MAJ Commentairesherbelin
2004-02-12Ajout delimiteur pour bool_scopeherbelin
2004-02-12Décomposition automatique des règles d'analyse syntaxique pour lesherbelin
2004-02-10backtrack implicit dans Bvectormarche
2004-02-09patch Bvector: args implicitesmarche
2004-01-27MAJ simplificationherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 08:03:56 +0000