aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Collapse)Author
2003-09-19Mise en place des V8Notation et V8Infix pour declarer des notations en v8 ↵herbelin
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
2003-09-12Suppression DatatypesSyntax et PeanoSyntax qui était videsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4383 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Bind et Delimit pour natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4370 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-11Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4353 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-10Affichage {}+{}, niveau paire au plus hautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4250 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-08recursion bien fondee sur des pairsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4224 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Suppression d'une occurrence superflue d'argument de type dans Notation ↵herbelin
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
2003-06-10Deplacement delimiteur T dans Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4130 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-29Bug niveauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4092 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-29Ne pas mettre d'associatif a droite au niveau 3 en V7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4088 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-27'only parsing' pour le passage de trucT a trucherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4084 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22V8Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4065 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22Ajout V8Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4061 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ↵herbelin
de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Blancsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3980 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-28Un principe light d'elimination de Acc, suivant les remarques de Yves Bertotletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3964 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17Intégration DatatypesSyntax à Datatypesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3945 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17Intégration DatatypesSyntax à Datatypesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3941 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17Syntaxe 'x=y:>T'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3940 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Activation des implicites pour la v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3886 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3881 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Suppression des alias eqT/exT/exT2 en nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3821 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Notation eqT superflueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3816 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
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
2003-03-29Déplacement de minus dans Peanoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3810 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-28notations <>, Assumption avec existentiel, replace termmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-21*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-14*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3770 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30Pb de parenthèse dans "Check (S (plus O O))"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3632 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-15Une entrée spéciale "annot" pour les piquantsherbelin
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
2002-12-15Ajout syntaxe '>'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3444 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-03Essai d'introduction d'un scope des typesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3363 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-29Re-échappement des \ et " dans les token stringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3339 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Simplificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3328 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Essai de suppression du caractere d'echappement des stringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3327 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Plus de précisionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3315 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27Retour sur associativité à droite de * pour compatibilité de prodherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3308 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Ne pas cacher les Metas d'une notations, ils peuvent être liant dansherbelin
les filtrage de ltac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3302 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Plus d'indication pour le gestionnaire de niveauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3292 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3290 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Bug niveauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3288 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25Retablissement SynDef Value/Errorherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3278 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25Oubliherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3277 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Généralisation de l'utilisation de Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3269 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-20Les parenthèses de la notation '(n)' maintemant mises par ML pour un ↵herbelin
meilleur affichage des entiers dans le scope nat_scope git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3261 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Oubliherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3234 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-07Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' ↵herbelin
comme un entier de nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3222 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-23Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourherbelin
compatibilité avec la surcharge dans certains développements (p.e. Utrecht/ABP) Déplacement de ~ au niveau 5 qui est le niveau des atomes propositionels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3175 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-22Redéplacement de + (sum) et * (prod) au niveau de + et * de ↵herbelin
l'arithmétique; ajout d'une option 'level' pour Notation; utilisation de Notation pour sumor et sumbool git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3173 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 15:09:06 +0000