| Age | Commit message (Expand) | Author |
| 2009-10-26 | New cleaning phase of the Local/Global option management | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2008-08-05 | Correction de bugs: | herbelin |
| 2008-06-16 | Add possibility to match on defined hypotheses, using brackets to | msozeau |
| 2008-05-11 | - Cleanup parsing of binders, reducing to a single production for all | msozeau |
| 2008-05-01 | Clarification de l'ordre d'interprétation des variables dans ltac. En | herbelin |
| 2008-04-29 | Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la | herbelin |
| 2008-04-14 | Diverses corrections | herbelin |
| 2008-02-10 | suppression code mort oublié lors du commit 10495 | herbelin |
| 2008-02-01 | Unification de TacLetRecIn et TacLetIn. En particulier, on peut | herbelin |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-07-16 | Generalized CAMLP4USE for pp dependencies | corbinea |
| 2007-04-02 | Extension to the general sequence operator (tactical). Now in addition to ... | emakarov |
| 2007-02-15 | Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lors | herbelin |
| 2006-11-02 | gestion speciale du niveau 5 des ltac | barras |
| 2006-10-31 | syntaxe du let in encore | barras |
| 2006-10-31 | assouplissement de la syntaxe du let de ltac: t1 ; let in autorise | barras |
| 2006-10-30 | fixed field_simplify + changed precedence of let and fun in ltac | barras |
| 2006-10-24 | Extension de la primitive ltac fresh pour qu'elle accepte une liste de | herbelin |
| 2006-07-11 | Utilisation du mot-clé lazymatch pour le match paresseux (à défaut d'avoir... | herbelin |
| 2006-05-30 | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin |
| 2006-03-05 | Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf... | herbelin |
| 2006-01-21 | Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f... | herbelin |
| 2005-12-26 | Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*... | herbelin |
| 2005-05-17 | Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux... | herbelin |
| 2004-10-11 | 'match term' now evaluates by default. Added 'lazy' keyword to delay the eval... | herbelin |
| 2004-07-16 | Suppression quotify | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-03-02 | Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation... | herbelin |
| 2004-03-01 | Généralisation du type ltac Identifier en IntroPattern; prise en compte des... | herbelin |
| 2004-01-02 | meilleure presentation des commentaires du traducteur | barras |
| 2003-11-12 | Idtac peut prendre un argument à afficher | narboux |
| 2003-10-16 | nouvelle syntaxe de ltac | barras |
| 2003-09-12 | Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c... | herbelin |
| 2003-05-24 | Ajout FreshId | herbelin |
| 2003-05-21 | Suppression définitive de lmatch et or_metanum dans tacinterp | herbelin |
| 2003-05-21 | Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ... | herbelin |
| 2003-05-19 | Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern | herbelin |
| 2003-04-07 | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin |
| 2003-03-31 | Ajout d'un message à FailTac | herbelin |
| 2003-03-14 | reparations suite a la nouvelle syntaxe: | barras |
| 2003-03-12 | *** empty log message *** | barras |
| 2003-01-19 | Restructuration interpréteur de tactique: plus d'évaluation partielle à la... | herbelin |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-10-14 | L'application de ltac attend une référence; meilleure protection contre | herbelin |
| 2002-10-13 | Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha... | herbelin |
| 2002-05-30 | Finalement un seul constr pour l'instant dans ExtraRedExpr | herbelin |
| 2002-05-29 | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin |
| 2002-05-27 | Ajout de Eval, Inst et Check | delahaye |
| 2002-05-15 | Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de | herbelin |