aboutsummaryrefslogtreecommitdiff
path: root/translate
AgeCommit message (Expand)Author
2003-09-21Renommages divers.herbelin
2003-09-21Mise en place d'implicites par noms en v8herbelin
2003-09-19parsingherbelin
2003-09-18Traduction de Instantiateherbelin
2003-09-18Niveau du 'as' des motifsherbelin
2003-09-16Pour appliquer les noms reserves aussi aux bindersherbelin
2003-09-12Mise en place affichage spécifique pour le scope des typesherbelin
2003-09-12Ajout 'Print Scopes' et 'Bind Scope with classes'; Mise en place affichage sp...herbelin
2003-09-10Passage des projections au niveau 1herbelin
2003-09-10Oubli des guillemets dans Commentsherbelin
2003-09-10Pretty-pretting fixherbelin
2003-09-09Traduction des réferences arguments de commandes non primitives; 'Grammar ta...herbelin
2003-09-09Ajout If; protection contre clash dans return_typeherbelin
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-06Mise en place possibilité de définitions locales dans les paramètres des i...herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 03:33:08 +0000