aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init
Commit message (Expand)AuthorAge
* 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
* Suppression des alias eqT/exT/exT2 en nouvelle syntaxeGravatar herbelin2003-03-31
* Notation eqT superflueGravatar herbelin2003-03-31
* eq fusionne avec eqT et devient par défaut sur Type,Gravatar herbelin2003-03-29
* Déplacement de minus dans PeanoGravatar herbelin2003-03-29
* notations <>, Assumption avec existentiel, replace termGravatar mohring2003-03-28
* *** empty log message ***Gravatar barras2003-03-21
* *** empty log message ***Gravatar barras2003-03-14
* *** empty log message ***Gravatar barras2003-03-12
* Pb de parenthèse dans "Check (S (plus O O))"Gravatar herbelin2003-01-30
* Une entrée spéciale "annot" pour les piquantsGravatar herbelin2002-12-15
* Ajout syntaxe '>'Gravatar herbelin2002-12-15
* Essai d'introduction d'un scope des typesGravatar herbelin2002-12-03
* Re-échappement des \ et " dans les token stringGravatar herbelin2002-11-29
* SimplificationGravatar herbelin2002-11-28
* Essai de suppression du caractere d'echappement des stringGravatar herbelin2002-11-28
* Plus de précisionsGravatar herbelin2002-11-28
* Retour sur associativité à droite de * pour compatibilité de prodGravatar herbelin2002-11-27
* Ne pas cacher les Metas d'une notations, ils peuvent être liant dansGravatar herbelin2002-11-26
* Plus d'indication pour le gestionnaire de niveauxGravatar herbelin2002-11-26
* Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiquesGravatar herbelin2002-11-26
* Bug niveauGravatar herbelin2002-11-26
* Retablissement SynDef Value/ErrorGravatar herbelin2002-11-25
* OubliGravatar herbelin2002-11-25
* Généralisation de l'utilisation de NotationGravatar herbelin2002-11-24
* Les parenthèses de la notation '(n)' maintemant mises par ML pour un meilleu...Gravatar herbelin2002-11-20
* OubliGravatar herbelin2002-11-14
* Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' co...Gravatar herbelin2002-11-07
* Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourGravatar herbelin2002-10-23
* Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...Gravatar herbelin2002-10-22
* Niveau d'affichage sumor/sumbool incohérent avec le parsingGravatar herbelin2002-10-21
* Prise en compte des délimiteurs dans les motifs de CasesGravatar herbelin2002-10-21
* Et 48, et 80, et 81, et 91, et 95, ... pour accommoder toujours plus de contribsGravatar herbelin2002-10-18
* Bugs dans la factorisation des règles de parsing de "{ ... } * ..."Gravatar herbelin2002-10-17
* Parsing des entiers de nat jusqu'à 29 pour accommoder certaines contribsGravatar herbelin2002-10-17
* La règle pour parser "(1)", "(2)", ... entre en conflit avec les expressionsGravatar herbelin2002-10-14
* Mise en place d'ensembles de notations symboliques pour nat, Z et RGravatar herbelin2002-10-13
* NettoyageGravatar herbelin2002-10-13
* Déplacement de + et * aux niveaux de précédence 7 et 6Gravatar herbelin2002-10-13
* Déplacement de + et * aux niveaux de précédence 7 et 6Gravatar herbelin2002-10-13
* Bug de précédenceGravatar herbelin2002-07-15
* Hack pour parser '{x:T|P}*B' sans parenthesesGravatar herbelin2002-07-11
* Utilisation d'Infix/Distfix autant que possibleGravatar herbelin2002-05-29
* petite erreur de syntaxeGravatar barras2002-05-14
* ajout des theoremes eqT_rec_r et eqT_rect_r pour RewriteGravatar barras2002-05-14
* lemmes plus_O_n et plus_Sn_m (pour Yves)Gravatar filliatr2002-05-07
* lemmes plus_O_n et plus_Sn_m (pour Yves)Gravatar filliatr2002-05-07
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
* DocGravatar herbelin2002-02-22