aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2003-12-21Affichage sur le modèle du forall pour le existsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5125 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-16Duplication temporaire des règles de syntaxe des pairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5102 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-05power associe a droitemarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5072 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-04Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace ↵herbelin
par un niveau ajoute dynamiquement; plus de limite vers le haut: divide au niveau 260 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5069 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-01Ratage standardisation Rge_monotony en Rmult_ge_compat_rherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5047 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵herbelin
par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Notation locale pour Rpowerherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5025 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Ajout lemmes, simplification preuve de SeqPropherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5024 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5022 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Utilisation du total_order non constructifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5019 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Report de lemmes de Znumtheory dans Zabs ou BinIntherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5018 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-28Protection contre les renommages; redondancesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5016 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-24Renoncement de la compatibilite des noms qualifies au profit de la ↵herbelin
compatibilite des arguments implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4979 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-22Compatibiliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4973 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Simplification; ajout Zcompare_antisymherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4965 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21ajout Pnat (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4964 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21ajout Pnat (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4963 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase ↵herbelin
et Pcompare_antisym git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4962 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Tri et typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4960 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19ajout de Znumtheory.v dans ZArithletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4952 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19Restauration compatibilite 7.4 pour le Hint Unfold Rgtherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4951 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Un nouveau lemme redondant ...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4934 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Deplacement ZERO_le_inj dans Zorderherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4933 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-15Meilleure solution pour la compatibiliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4921 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Pour les .v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4917 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_baseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4914 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4912 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Presentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4911 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Ordre standard pour l'associativiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4908 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Quelques oublis pour que les notations marchent bienherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4907 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Bug implicit argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4905 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Automatisation de la traduction de iff_trans; renommage IFherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4903 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Backtrack sur Peanoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4902 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Nouveaux lemmes 'canoniques'; compatibiliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4901 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13moins unaire au niveau 35, tactiques simple_induction et simple_destruct, ↵barras
Local devient Let git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4897 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13Oubli report Nul/Posherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4895 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13Requireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4889 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13qq petit ajouts à Zdivletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4888 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12MAJ INZherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4886 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Ajout lemme projectionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4883 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12%type au lieu de %Therbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4882 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Lemmes dans un sens plus naturelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4881 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Restructuration ZArithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4879 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4878 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Noms canoniques pour les variables lieesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4877 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Independance vis a vis noms variables liees; partie sur bool dans Zboolherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4876 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Noms/énoncés plus canoniquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4875 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Independance vis a vis noms variables lieesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4874 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Ajout lemmes; independance vis a vis noms variables liees; restructurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4873 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 13:45:45 +0000