aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init
Commit message (Collapse)AuthorAge
* Fusion des fichiers de syntaxe de Init avec les fichiers de définition; ↵Gravatar herbelin2003-09-23
| | | | | | TypeSyntax inutile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4461 85f007b7-540e-0410-9357-904b9bb8a0f7
* traducteur: affiche les commentaires a l'interieur des commandesGravatar barras2003-09-22
| | | | | | | extraction: pb avec les variables de section definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant ↵Gravatar herbelin2003-09-21
| | | | | | aussi à nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4428 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant ↵Gravatar herbelin2003-09-21
| | | | | | aussi à nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4427 85f007b7-540e-0410-9357-904b9bb8a0f7
* NettoyageGravatar herbelin2003-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place des V8Notation et V8Infix pour declarer des notations en v8 ↵Gravatar herbelin2003-09-19
| | | | | | meme si incompatible avec la syntaxe v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4417 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression DatatypesSyntax et PeanoSyntax qui était videsGravatar herbelin2003-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4383 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bind et Delimit pour natGravatar herbelin2003-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4370 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...Gravatar herbelin2003-09-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4353 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage {}+{}, niveau paire au plus hautGravatar herbelin2003-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4250 85f007b7-540e-0410-9357-904b9bb8a0f7
* recursion bien fondee sur des pairsGravatar filliatr2003-07-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4224 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
* 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
* 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
* BlancsGravatar herbelin2003-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3980 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
* 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
* Activation des implicites pour la v8Gravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3886 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"Gravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3881 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des alias eqT/exT/exT2 en nouvelle syntaxeGravatar herbelin2003-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notation eqT superflueGravatar herbelin2003-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3816 85f007b7-540e-0410-9357-904b9bb8a0f7
* eq fusionne avec eqT et devient par défaut sur Type,Gravatar herbelin2003-03-29
| | | | | | | idem pour ex et exT, ex2 et exT2, all et allT git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3812 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de minus dans PeanoGravatar herbelin2003-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3810 85f007b7-540e-0410-9357-904b9bb8a0f7
* notations <>, Assumption avec existentiel, replace termGravatar mohring2003-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3770 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pb de parenthèse dans "Check (S (plus O O))"Gravatar herbelin2003-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3632 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une entrée spéciale "annot" pour les piquantsGravatar herbelin2002-12-15
| | | | | | | Positionnement du scope type_scope à certains endroits bien choisis git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3445 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout syntaxe '>'Gravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3444 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai d'introduction d'un scope des typesGravatar herbelin2002-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-échappement des \ et " dans les token stringGravatar herbelin2002-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3339 85f007b7-540e-0410-9357-904b9bb8a0f7
* SimplificationGravatar herbelin2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3328 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai de suppression du caractere d'echappement des stringGravatar herbelin2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3327 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de précisionsGravatar herbelin2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3315 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour sur associativité à droite de * pour compatibilité de prodGravatar herbelin2002-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3308 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ne pas cacher les Metas d'une notations, ils peuvent être liant dansGravatar herbelin2002-11-26
| | | | | | | les filtrage de ltac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3302 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus d'indication pour le gestionnaire de niveauxGravatar herbelin2002-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3292 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiquesGravatar herbelin2002-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3290 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug niveauGravatar herbelin2002-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3288 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retablissement SynDef Value/ErrorGravatar herbelin2002-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3278 85f007b7-540e-0410-9357-904b9bb8a0f7
* OubliGravatar herbelin2002-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3277 85f007b7-540e-0410-9357-904b9bb8a0f7
* Généralisation de l'utilisation de NotationGravatar herbelin2002-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3269 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 20:34:28 +0000