aboutsummaryrefslogtreecommitdiff
path: root/translate
AgeCommit message (Expand)Author
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-03Affichage des 'fun' suivis de 'let' en utilisant explicitement un 'let'herbelin
2003-09-02Contorsions pour que l'interpretation deses foncteurs depende des parametres ...herbelin
2003-09-02Bug traduction Search, SearchPattern, etc.herbelin
2003-08-31Bug et améliorations diversherbelin
2003-08-14Amélioration affichage syntaxe modulesherbelin
2003-08-13Hack pour ajouter Proof apres Correctnessherbelin
2003-08-12Bug et amliorations diversesherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-06-23Ajout systématique de Proof dans la traductionherbelin
2003-06-23Formattage Apply withherbelin
2003-06-23Formattage pattern 'match'herbelin
2003-06-19Ajout 'Symmetry in Hyp'; chgt syntaxe 'change ... with ...'herbelin
2003-06-14Ajout option Local à Hint, Hints et HintDestructherbelin
2003-06-13Utilisation de intro_pattern dans NewDestruct/NewInductionherbelin
2003-06-12Ajout option translate_syntax pour caractériser l'interprétation du traduct...herbelin
2003-06-10Ajout notation c.(f) en v8 pour les projections de Record; raffinement diversherbelin
2003-06-10Raffinement diversherbelin
2003-06-10Globalisation des tactiques avant traduction pour capture des noms; affinemen...herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 20:33:18 +0000