aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
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
2003-04-28Localisation erreurs TacAlias; Globalisation moins tolérante dans lesherbelin
2003-04-27Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...herbelin
2003-04-27Reparation affichage LetTacherbelin
2003-04-25extension des caracteres UTF 8 autorises dans les symbolesfilliatr
2003-04-17Ajout "at next level" dans Notationherbelin
2003-04-16simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...letouzey
2003-04-14Localisation des appels de tactiques définies sans argumentsherbelin
2003-04-14Correction bug PR#278coq
2003-04-11Ajout option 'Local' à Infix et Notationherbelin
2003-04-10Affichage forcé des implicites contextuels si pas de contexte connuherbelin
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
2003-04-08Ajout option "Local" à "Open Scope"herbelin
2003-04-07lconstr pour genterm en v8herbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-04-07Ajout cas Matchherbelin
2003-04-07Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun impliciteherbelin
2003-04-07Options d'affichage maintenant dans Constrexternherbelin
2003-04-02espace manquantherbelin
2003-03-31Ajout d'un message à FailTacherbelin
2003-03-31Bug pattern_occ_hyp_listherbelin
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
2003-03-28notations <>, Assumption avec existentiel, replace termmohring
2003-03-27MAJ des mots-clés, Definition, Theorem, ...herbelin
2003-03-27MAJ des mots-clés, Definition, Theorem, ...herbelin
2003-03-27Affinement nommage des productionsherbelin
2003-03-21*** empty log message ***barras
2003-03-14reparations suite a la nouvelle syntaxe:barras
2003-03-13Ajout réaffichage SubClassherbelin
2003-03-12*** empty log message ***barras
2003-03-12Renommage indpar pour usage plus generalherbelin
2003-03-04Bug délimiteur de scope en vieil affichage astherbelin
2003-03-03Retour vieil afficheurherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 16:56:38 +0000