aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* AVL: suiteGravatar filliatr2003-06-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4174 85f007b7-540e-0410-9357-904b9bb8a0f7
* AVL de caml: un debutGravatar filliatr2003-06-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4173 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground depthGravatar filliatr2003-06-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4170 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation fsets suite a changement de GroundGravatar filliatr2003-06-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement de le_minus de fast_integer vers MinusGravatar herbelin2003-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4162 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement de le_minus de fast_integer vers MinusGravatar herbelin2003-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4161 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement de spécif du foldGravatar letouzey2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4159 85f007b7-540e-0410-9357-904b9bb8a0f7
* fcts tail-recursivesGravatar filliatr2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4153 85f007b7-540e-0410-9357-904b9bb8a0f7
* Require ExportGravatar filliatr2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4152 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSets, mais pas compile' par make worldGravatar filliatr2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4150 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite changements ZArith en vu de librairie FSetGravatar letouzey2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4149 85f007b7-540e-0410-9357-904b9bb8a0f7
* quelques adaptations de Zarith en vu de la nouvelle librarie FSetGravatar letouzey2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4148 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement d'un lemme sur nat de ZArith vers ArithGravatar herbelin2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4146 85f007b7-540e-0410-9357-904b9bb8a0f7
* INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le ↵Gravatar herbelin2003-06-12
| | | | | | traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4140 85f007b7-540e-0410-9357-904b9bb8a0f7
* Import nat_scopeGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4132 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression d'une occurrence superflue d'argument de type dans Notation ↵Gravatar herbelin2003-06-10
| | | | | | sachant que les 2 occurrences ne sont pas forcement dans le meme scope git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement delimiteur T dans NotationsGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4130 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug niveauGravatar herbelin2003-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4092 85f007b7-540e-0410-9357-904b9bb8a0f7
* niveau 49 devient nextGravatar herbelin2003-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4091 85f007b7-540e-0410-9357-904b9bb8a0f7
* niveau 49 devient nextGravatar herbelin2003-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4089 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ne pas mettre d'associatif a droite au niveau 3 en V7Gravatar herbelin2003-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4088 85f007b7-540e-0410-9357-904b9bb8a0f7
* 'only parsing' pour le passage de trucT a trucGravatar herbelin2003-05-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4084 85f007b7-540e-0410-9357-904b9bb8a0f7
* "INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans RealsGravatar herbelin2003-05-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4074 85f007b7-540e-0410-9357-904b9bb8a0f7
* V8NotationGravatar herbelin2003-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout V8NotationGravatar herbelin2003-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4061 85f007b7-540e-0410-9357-904b9bb8a0f7
* Concentration des notations officielles dans Init/Notations; restructuration ↵Gravatar herbelin2003-05-21
| | | | | | de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
* NotationsGravatar herbelin2003-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4047 85f007b7-540e-0410-9357-904b9bb8a0f7
* BugGravatar herbelin2003-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amelioration presentationGravatar herbelin2003-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amelioration affichageGravatar herbelin2003-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4019 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de 'R' dans la notation == entreGravatar herbelin2003-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4016 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de 'R' dans la notation == entreGravatar herbelin2003-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4015 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement lemmes sur fact de Reals vers ArithGravatar herbelin2003-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4014 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux lemmesGravatar herbelin2003-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4013 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux lemmes (sur proposition de Nijmegen)Gravatar herbelin2003-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4012 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux lemmes (sur proposition de Nijmegen)Gravatar herbelin2003-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4010 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout inverse relation bien fondeeGravatar mohring2003-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4000 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: toolbar/autosaveGravatar monate2003-05-07
| | | | | | | Hugo: Suppression du type dans les notations == et <> entre git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3992 85f007b7-540e-0410-9357-904b9bb8a0f7
* BlancsGravatar herbelin2003-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3980 85f007b7-540e-0410-9357-904b9bb8a0f7
* NotationsGravatar herbelin2003-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3979 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implicit TypesGravatar herbelin2003-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3978 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout ChoiceFactsGravatar herbelin2003-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3977 85f007b7-540e-0410-9357-904b9bb8a0f7
* BlancsGravatar herbelin2003-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3976 85f007b7-540e-0410-9357-904b9bb8a0f7
* En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ↵Gravatar herbelin2003-04-29
| | | | | | Rlt_sym, Rle_sym; utilisation de la terminologie 'commutative' plutôt que 'symétrie' pour les opérateurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un principe light d'elimination de Acc, suivant les remarques de Yves BertotGravatar letouzey2003-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3964 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration DatatypesSyntax à DatatypesGravatar herbelin2003-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3945 85f007b7-540e-0410-9357-904b9bb8a0f7
* DiversGravatar herbelin2003-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3943 85f007b7-540e-0410-9357-904b9bb8a0f7
* <> maintenant standardGravatar herbelin2003-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3942 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration DatatypesSyntax à DatatypesGravatar herbelin2003-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3941 85f007b7-540e-0410-9357-904b9bb8a0f7
* Syntaxe 'x=y:>T'Gravatar herbelin2003-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3940 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 15:51:29 +0000