aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Deplacement de le_minus de fast_integer vers MinusGravatar herbelin2003-06-14
* Deplacement de le_minus de fast_integer vers MinusGravatar herbelin2003-06-14
* majGravatar filliatr2003-06-14
* changement de spécif du foldGravatar letouzey2003-06-13
* Ground updateGravatar corbinea2003-06-13
* CoqIDE: undo plus efficace sur les inductifsGravatar filliatr2003-06-13
* Ground update, new files.Gravatar corbinea2003-06-13
* coqide: indentationGravatar monate2003-06-13
* Utilisation de intro_pattern dans NewDestruct/NewInductionGravatar herbelin2003-06-13
* fcts tail-recursivesGravatar filliatr2003-06-13
* Require ExportGravatar filliatr2003-06-13
* install-fsetsGravatar filliatr2003-06-13
* FSets, mais pas compile' par make worldGravatar filliatr2003-06-13
* suite changements ZArith en vu de librairie FSetGravatar letouzey2003-06-13
* quelques adaptations de Zarith en vu de la nouvelle librarie FSetGravatar letouzey2003-06-13
* coqide: about now displays versions/Fix for alt-enterGravatar monate2003-06-13
* Deplacement d'un lemme sur nat de ZArith vers ArithGravatar herbelin2003-06-13
* CoqIDE: undo immediat sur les commandes ne modifiant pas l'etatGravatar filliatr2003-06-13
* Ground update.Gravatar corbinea2003-06-13
* enieme correction du nommage modulaireGravatar letouzey2003-06-12
* fin de l'affichage des signatures de modules dans les *.mlGravatar letouzey2003-06-12
* MAJGravatar herbelin2003-06-12
* INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le tradu...Gravatar herbelin2003-06-12
* Ajout option translate_syntax pour caractériser l'interprétation du traduct...Gravatar herbelin2003-06-12
* Pb quand une meme classe est definie dans 2 fichiersGravatar herbelin2003-06-11
* Token '.(' seulement pour v8, sinon conflit avec '.(*'Gravatar herbelin2003-06-11
* majGravatar filliatr2003-06-11
* MAJGravatar herbelin2003-06-10
* TypoGravatar herbelin2003-06-10
* Module Bij inutiliseGravatar herbelin2003-06-10
* Import nat_scopeGravatar herbelin2003-06-10
* Suppression d'une occurrence superflue d'argument de type dans Notation sacha...Gravatar herbelin2003-06-10
* Deplacement delimiteur T dans NotationsGravatar herbelin2003-06-10
* Module Bij inutiliseGravatar herbelin2003-06-10
* Ajout notation c.(f) en v8 pour les projections de RecordGravatar herbelin2003-06-10
* freshid -> freshGravatar herbelin2003-06-10
* Déplacement traducteur de nom dans Constrextern pour accès aux noms longsGravatar herbelin2003-06-10
* Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...Gravatar herbelin2003-06-10
* Simplification case_infoGravatar herbelin2003-06-10
* Ajout notation c.(f) en v8 pour les projections de Record; raffinement diversGravatar herbelin2003-06-10
* Raffinement diversGravatar herbelin2003-06-10
* Globalisation des tactiques avant traduction pour capture des noms; affinemen...Gravatar herbelin2003-06-10
* Distinction mode v7 ou translate; conséquences du déplacement traducteur de...Gravatar herbelin2003-06-10
* Déplacement de code dans command; MAJ DebugOnGravatar herbelin2003-06-10
* Mise en place structure pour des 'arguments scope' dirigés par une classeGravatar herbelin2003-06-10
* Amélioration afficheur de Cases pour les constr_patternGravatar herbelin2003-06-10
* Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...Gravatar herbelin2003-06-10
* Déplacement traducteur de nom dans Constrextern pour accès aux noms longsGravatar herbelin2003-06-10
* Ajout notation c.(f) en v8 pour les projections de RecordGravatar herbelin2003-06-10
* Factorisation de detype_case pour utilisation par l'afficheur de patternGravatar herbelin2003-06-10