aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2003-09-12Ajout 'Print Scopes' et 'Bind Scope with classes'; 'Delimits' -> 'Delimit'herbelin
2003-09-10Passage des projections au niveau 1herbelin
2003-09-109 est associatif a gaucheherbelin
2003-09-10Traduction de Distfixherbelin
2003-09-09Ajout construction If primitive dans constr_expr et rawconstrherbelin
2003-09-09'Grammar tactic' devient 'Tactic Notation'herbelin
2003-09-09Traduction des réferences arguments de commandes non primitivesherbelin
2003-09-09Code mortherbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des r...herbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des r...herbelin
2003-09-06Paramétrisation vis à vis de existential_keyherbelin
2003-09-06'Implicits qid' -> 'Implicit Arguments qid'herbelin
2003-09-06Adapter l'entree de grammaire a la version 7 ou 8herbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des i...herbelin
2003-09-06Passage de lconstr à constr pour les arguments immédiat de commandesherbelin
2003-09-06Passage de lconstr à constr pour les arguments immédiat de commandesherbelin
2003-09-06Bug affichage tactiques supplementaires en v8 (suite)herbelin
2003-09-05Bug affichage tactiques supplementaires en v8herbelin
2003-09-05Impression sans ',' des constructeurs de meme type, pour v8herbelin
2003-09-02Relachement conflit 'with' dans le cas des Module with Definitionherbelin
2003-08-31'Assumptions' sur le modèle général des lieursherbelin
2003-08-31Affichage des inductifs en v8herbelin
2003-08-14Pb de mot-cleherbelin
2003-08-14Ajout token '!' pour correctnessherbelin
2003-08-14Enregistrement tuple_constrherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-06-20Bug compilationherbelin
2003-06-19Ajout 'Symmetry in Hyp'herbelin
2003-06-19Ajout 'Symmetry in Hyp'; chgt syntaxe 'change ... with ...'herbelin
2003-06-17Ajout option Local aux Hintherbelin
2003-06-14Ajout option Local à Hint, Hints et HintDestructherbelin
2003-06-13Utilisation de intro_pattern dans NewDestruct/NewInductionherbelin
2003-06-11Token '.(' seulement pour v8, sinon conflit avec '.(*'herbelin
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
2003-06-10freshid -> freshherbelin
2003-06-08Tables logarithmiques pour les coercions + nettoyageherbelin
2003-05-26Bugherbelin
2003-05-24Ajout FreshIdherbelin
2003-05-22Ajout V8Notationherbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...herbelin
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...herbelin
2003-05-21Possibilité de syntaxe conjointement à la définition des inductifs et des ...herbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-05-08Petite correction d'affichage de modulescoq
2003-04-29Prise en compte des syntaxes v8 dans Uninterpreted Notationherbelin
2003-04-29Prise en compte des syntaxes v8 dans Uninterpreted Notationherbelin
2003-04-29Factorisation des produits de même type; parenthèses autour des x:=c et n:=...herbelin
2003-04-29Factorisation des produits de même type; parenthèses autour des x:=c et n:=...herbelin
2003-04-29Ajout is_ident_tailherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 16:39:46 +0000