| Age | Commit message (Expand) | Author |
|---|
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-10-01 | Added a new tactical infoH tac, that displays the names of hypothesis created... | courtieu |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-19 | Getting rid of the undocumented [complete] tactic, which was | ppedrot |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-05-30 | Restore compatibility with camlp4 (some missing open Tok) | letouzey |
| 2012-05-29 | Migrate the grammar entry about "Ltac" into g_vernac.ml4. | letouzey |
| 2012-05-29 | simplification in deps of some g_*.ml4 | letouzey |
| 2012-05-29 | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey |
| 2012-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-05-29 | Vernacexpr is now a mli-only file, locality stuff now in locality.ml | letouzey |
| 2011-11-17 | Fixing bug #2640 and variants of it (inconsistency between when and | herbelin |
| 2011-03-18 | A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds | letouzey |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-05-19 | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey |
| 2010-05-19 | static (and shared) camlp4use instead of per-file declaration | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 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 |
