aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2002-12-19Petit netoyage dans libcoq
2002-12-19suite du commit precedentbarras
2002-12-15Prise en compte des scopes traversés dans les notationsherbelin
2002-12-12Ajout du vernac Proof withgregoire
2002-12-10Ajout options -v7 et -v8, et commandes V7only et V8onlyherbelin
2002-12-10Ajout options -v7 et -v8, et commandes V7only et V8onlyherbelin
2002-12-09Problèmes et améliorations divers affichageherbelin
2002-12-09Code mort ?herbelin
2002-12-04Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...herbelin
2002-12-04Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...herbelin
2002-12-04Modification Require Frommohring
2002-12-03la table PARAMETER n'existe plus (mergé dans la table CONSTANT)letouzey
2002-12-03Préparation à la prise en compte des changements de scopes internes aux not...herbelin
2002-12-03Pas de globalisation impérative pour les Grammarherbelin
2002-12-02Re-déplacement du résultat de Grammar au niveau constr_expr (globalisation ...herbelin
2002-12-02Ajout des options "Set Contextual Implicits" et "Set Strict Implicitsherbelin
2002-12-02On force l'associativité pour les entrées sans niveauxherbelin
2002-11-29Raffinement syntaxe Infixherbelin
2002-11-28Affinement de la gestion des niveaux toujours; type ETBigintherbelin
2002-11-28typo ?letouzey
2002-11-28Affinement encoreherbelin
2002-11-27Ajout répertoire interpherbelin
2002-11-26Réaffichage des Syntactic Definition (printer constr_expr).herbelin
2002-11-25Syntaxe delimiteursherbelin
2002-11-25MAJ delimiters et niveaux d'associativiteherbelin
2002-11-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...herbelin
2002-11-19Autoriser les abbreviations de Casesherbelin
2002-11-15Passage à une représentation des fixpoints plus primitive dans constr_expr ...herbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-06Un Local construit par preuve hors section doit être considéré globalherbelin
2002-11-05Intégration des modifs de la branche mowgli :herbelin
2002-11-05Nouvelle option -xml à coqtop pour compiler un développement enherbelin
2002-10-30Optimisation du choix des niveaux intermédiaires dans une notation complexeherbelin
2002-10-26code mortherbelin
2002-10-23Clarification changements autour de Remark/Fact/Localherbelin
2002-10-23Le test de redondance d'une règle était trop fortherbelin
2002-10-22Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...herbelin
2002-10-21Prise en compte des délimiteurs dans les motifs de Casesherbelin
2002-10-16Réparation du mécanisme des infixes quand ils commencent par une lettreherbelin
2002-10-14Meilleure analyse de si une règle de grammaire/syntaxe existent déjà ou pasherbelin
2002-10-14Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'uneherbelin
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin
2002-10-09retour en arriere concernant la recherche d'occurence modulo expansion des le...barras
2002-09-29Que des niveaux d'univers frais dans le type des constantes globalesherbelin
2002-09-29Que des niveaux d'univers frais dans le type des constantes globalesherbelin
2002-09-27Encore quelques rangements dans Nametab + petits trucscoq
2002-09-24Nametab data structure reorganisationcoq
2002-09-20La notation with dependante + affichage dependante de moduels corrigecoq
2002-09-03pretyping/pretyping.mlherbelin
2002-08-19Pretty-printing preliminaire des modules, commandescoq
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 00:20:13 +0000