aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Suppression d'une occurrence superflue d'argument de type dans Notation sacha...Gravatar herbelin2003-06-10
* Deplacement delimiteur T dans NotationsGravatar herbelin2003-06-10
* Bug niveauGravatar herbelin2003-05-29
* niveau 49 devient nextGravatar herbelin2003-05-29
* niveau 49 devient nextGravatar herbelin2003-05-29
* Ne pas mettre d'associatif a droite au niveau 3 en V7Gravatar herbelin2003-05-29
* 'only parsing' pour le passage de trucT a trucGravatar herbelin2003-05-27
* "INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans RealsGravatar herbelin2003-05-24
* V8NotationGravatar herbelin2003-05-22
* Ajout V8NotationGravatar herbelin2003-05-22
* Concentration des notations officielles dans Init/Notations; restructuration ...Gravatar herbelin2003-05-21
* NotationsGravatar herbelin2003-05-21
* BugGravatar herbelin2003-05-21
* Amelioration presentationGravatar herbelin2003-05-14
* Amelioration affichageGravatar herbelin2003-05-14
* Suppression de 'R' dans la notation == entreGravatar herbelin2003-05-14
* Suppression de 'R' dans la notation == entreGravatar herbelin2003-05-14
* Deplacement lemmes sur fact de Reals vers ArithGravatar herbelin2003-05-14
* Nouveaux lemmesGravatar herbelin2003-05-13
* Nouveaux lemmes (sur proposition de Nijmegen)Gravatar herbelin2003-05-13
* Nouveaux lemmes (sur proposition de Nijmegen)Gravatar herbelin2003-05-13
* ajout inverse relation bien fondeeGravatar mohring2003-05-09
* coqide: toolbar/autosaveGravatar monate2003-05-07
* BlancsGravatar herbelin2003-04-29
* NotationsGravatar herbelin2003-04-29
* Implicit TypesGravatar herbelin2003-04-29
* Ajout ChoiceFactsGravatar herbelin2003-04-29
* BlancsGravatar herbelin2003-04-29
* En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...Gravatar herbelin2003-04-29
* Un principe light d'elimination de Acc, suivant les remarques de Yves BertotGravatar letouzey2003-04-28
* Intégration DatatypesSyntax à DatatypesGravatar herbelin2003-04-17
* DiversGravatar herbelin2003-04-17
* <> maintenant standardGravatar herbelin2003-04-17
* Intégration DatatypesSyntax à DatatypesGravatar herbelin2003-04-17
* Syntaxe 'x=y:>T'Gravatar herbelin2003-04-17
* suite au commit d'hugo dans TypeSyntax & Raxiom, Intro donnait un nom differentGravatar letouzey2003-04-16
* sumboolT, sumorT, sigTT, SigT redondantsGravatar herbelin2003-04-16
* CosmetiqueGravatar herbelin2003-04-14
* Local 'o'Gravatar herbelin2003-04-14
* Open Scope en LocalGravatar herbelin2003-04-12
* Open Scope remplace ImportGravatar herbelin2003-04-10
* Calcul automatique de l'implicite de nil pour que l'affichage sache le traiterGravatar herbelin2003-04-10
* Remplacement Import par Open Scope en v8Gravatar herbelin2003-04-10
* cast de nilGravatar herbelin2003-04-09
* nil en implicite dans la v8Gravatar herbelin2003-04-09
* Ajout Open ScopeGravatar herbelin2003-04-09
* Activation des implicites pour la v8Gravatar herbelin2003-04-09
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"Gravatar herbelin2003-04-09
* Renommage K; equivalence JMeq et eq_dep sur TypeGravatar herbelin2003-04-09
* DefinedGravatar herbelin2003-04-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 11:36:49 +0000