aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
...
* Tri et typoGravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4960 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de Znumtheory.v dans ZArithGravatar letouzey2003-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restauration compatibilite 7.4 pour le Hint Unfold RgtGravatar herbelin2003-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4951 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un nouveau lemme redondant ...Gravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4934 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement ZERO_le_inj dans ZorderGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4933 85f007b7-540e-0410-9357-904b9bb8a0f7
* Meilleure solution pour la compatibiliteGravatar herbelin2003-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4921 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour les .v8Gravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_baseGravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4914 85f007b7-540e-0410-9357-904b9bb8a0f7
* cosmetiqueGravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4912 85f007b7-540e-0410-9357-904b9bb8a0f7
* PresentationGravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4911 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ordre standard pour l'associativiteGravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4908 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques oublis pour que les notations marchent bienGravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4907 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug implicit argumentsGravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4905 85f007b7-540e-0410-9357-904b9bb8a0f7
* Automatisation de la traduction de iff_trans; renommage IFGravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4903 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur PeanoGravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4902 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux lemmes 'canoniques'; compatibiliteGravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4901 85f007b7-540e-0410-9357-904b9bb8a0f7
* moins unaire au niveau 35, tactiques simple_induction et simple_destruct, ↵Gravatar barras2003-11-13
| | | | | | Local devient Let git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4897 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli report Nul/PosGravatar herbelin2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4895 85f007b7-540e-0410-9357-904b9bb8a0f7
* RequireGravatar herbelin2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4889 85f007b7-540e-0410-9357-904b9bb8a0f7
* qq petit ajouts à ZdivGravatar letouzey2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4888 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ INZGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4886 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout lemme projectionsGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4883 85f007b7-540e-0410-9357-904b9bb8a0f7
* %type au lieu de %TGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4882 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lemmes dans un sens plus naturelGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4881 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration ZArithGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4879 85f007b7-540e-0410-9357-904b9bb8a0f7
* CosmetiqueGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4878 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noms canoniques pour les variables lieesGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Independance vis a vis noms variables liees; partie sur bool dans ZboolGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4876 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noms/énoncés plus canoniquesGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4875 85f007b7-540e-0410-9357-904b9bb8a0f7
* Independance vis a vis noms variables lieesGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4874 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout lemmes; independance vis a vis noms variables liees; restructurationGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4873 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout partie sur bool anciennement dans ZmiscGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4872 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout lemmes; independance vis a vis noms variables lieesGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4871 85f007b7-540e-0410-9357-904b9bb8a0f7
* On sait jamaisGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4862 85f007b7-540e-0410-9357-904b9bb8a0f7
* petits changements de syntaxeGravatar barras2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout quelques lemmes; noms des variables lieesGravatar herbelin2003-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4845 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli BinNatGravatar herbelin2003-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4826 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli d'un Set Implicit ArgumentsGravatar herbelin2003-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4825 85f007b7-540e-0410-9357-904b9bb8a0f7
* Biblio standard sans mention de la possibilite d'etre impredicatifGravatar herbelin2003-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4823 85f007b7-540e-0410-9357-904b9bb8a0f7
* Biblio standard sans impredicativiteGravatar herbelin2003-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4822 85f007b7-540e-0410-9357-904b9bb8a0f7
* Des oublisGravatar herbelin2003-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4819 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report des definitions sorties de fast_integer pour compatibiliteGravatar herbelin2003-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4818 85f007b7-540e-0410-9357-904b9bb8a0f7
* NotationsGravatar herbelin2003-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4816 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout répertoire NArith pour l'arithmétique binaire sur les nombres ↵Gravatar herbelin2003-11-05
| | | | | | positifs et naturels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4809 85f007b7-540e-0410-9357-904b9bb8a0f7
* Preuve de l'incoherence de {A}+{~A} avec Set impredicatifGravatar herbelin2003-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4808 85f007b7-540e-0410-9357-904b9bb8a0f7
* RedondancesGravatar herbelin2003-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration ZArith et déport de la partie sur 'positive' dans NArith, ↵Gravatar herbelin2003-11-05
| | | | | | de la partie Omega dans contrib/omega git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4801 85f007b7-540e-0410-9357-904b9bb8a0f7
* Exporting ^; utilisation arg scope impliciteGravatar herbelin2003-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4783 85f007b7-540e-0410-9357-904b9bb8a0f7
* CosmetiqueGravatar herbelin2003-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4780 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renforcement significatif du resultat principalGravatar herbelin2003-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4779 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 15:50:55 +0000