aboutsummaryrefslogtreecommitdiff
path: root/translate
AgeCommit message (Expand)Author
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-21Possibilité de syntaxe conjointement à la définition des inductifs et des ...herbelin
2003-05-20Prise en compte notation dans Inductif pour traducteurherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-05-13Separation entre les propositions de syntaxe - suiteherbelin
2003-05-13Separation entre les 2 propositions de syntaxeherbelin
2003-05-07coqide: toolbar/autosavemonate
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-28Localisation erreurs TacAlias; Globalisation moins tolérante dans lesherbelin
2003-04-27Reparation affichage LetTacherbelin
2003-04-17Ajout "at next level" dans Notationherbelin
2003-04-14Localisation des appels de tactiques définies sans argumentsherbelin
2003-04-11Ajout option 'Local' à Infix et Notationherbelin
2003-04-10Affichage des inductifsherbelin
2003-04-09Affichage des inductifsherbelin
2003-04-09Formattage affichageherbelin
2003-04-09Mécanisme plus simple et efficace pour traduire les implicitesherbelin
2003-04-09Bugs synchronisation pour gestion traduction des implicitesherbelin
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
2003-04-08Ajout option "Local" à "Open Scope"herbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-04-07Aérer les := et : de "assert"herbelin
2003-04-07Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun impliciteherbelin
2003-03-31Ajout d'un message à FailTacherbelin
2003-03-31Ajout VernacReserve et suppression des types re-inferablesherbelin
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
2003-03-21*** empty log message ***barras
2003-03-13Ajout réaffichage SubClassherbelin
2003-03-12*** empty log message ***barras
2003-03-12Ajout Locate Notationherbelin
2003-02-05updatedesmettr
2003-02-05Ajout du traducteurdesmettr
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 07:15:33 +0000