| Age | Commit message (Expand) | Author |
|---|
| 2010-05-18 | Applicative commutative cuts in Fixpoint guard condition | pboutill |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2009-11-08 | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-06-11 | Use a lazy value for the message in FailError, so that it won't be | msozeau |
| 2009-04-24 | Fixing bug #2308 ("instantiate" tactic did not comply with | herbelin |
| 2009-03-17 | Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl) | herbelin |
| 2009-03-16 | Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4" | herbelin |
| 2009-03-14 | Cleaning/uniformizing the interface of tacticals.mli | herbelin |
| 2009-01-23 | Petit nettoyage faisant suite au commit #11847 . | aspiwack |
| 2009-01-02 | - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H", | herbelin |
| 2008-12-26 | - Extracted from the tactic "now" an experimental tactic "easy" for small | herbelin |
| 2008-12-26 | - Optimized "auto decomp" which had a (presumably) exponential in | herbelin |
| 2008-10-22 | Affichage des notations récursives: | herbelin |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2008-06-21 | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin |
| 2008-06-10 | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin |
| 2008-04-27 | - Backtrack sur option with_types suite à confusion sur l'utilisation | herbelin |
| 2008-04-26 | - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec | herbelin |
| 2008-04-13 | Bugs, nettoyage, et améliorations diverses | herbelin |
| 2008-04-04 | Mise en place d'une extension de apply pour que celui-ci sache | herbelin |
| 2007-12-07 | Adding the tactic "instantiate" (without argument), to force the | glondu |
| 2007-05-22 | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin |
| 2006-10-05 | revision de la semantique de rewrite ... in <clause>. details dans la doc | letouzey |
| 2006-05-30 | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin |
| 2006-01-21 | Messages de idtac et fail peuvent maintenant être des listes de string, int ... | herbelin |
| 2006-01-16 | Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-11-02 | Types inductifs parametriques | mohring |
| 2004-11-16 | IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name). | sacerdot |
| 2004-10-20 | COMMITED BYTECODE COMPILER | barras |
| 2004-09-15 | hiding the meta_map in evar_defs | barras |
| 2004-09-10 | simplification de clenv | barras |
| 2004-09-08 | unification encore... | barras |
| 2004-09-07 | deuxieme vague de modifs: evar_defs fonctionnel | barras |
| 2004-09-03 | premiere reorganisation de l\'unification | barras |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-03-02 | Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va... | herbelin |
| 2004-03-01 | Déplacement définition intro_pattern_expr dans Genarg | herbelin |
| 2003-11-13 | factorisation et generalisation des clauses | barras |
| 2003-11-12 | Idtac peut prendre un argument à afficher | narboux |
| 2003-10-10 | Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion' | herbelin |
| 2003-09-12 | Indépendance vis à vis de Declare | herbelin |
| 2003-06-20 | Ground Update. | corbinea |
| 2003-04-07 | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin |
| 2003-03-31 | Ajout d'un message à FailTac | herbelin |
| 2002-08-02 | Modules dans COQ\!\!\!\! | coq |
| 2002-05-29 | Réorganisation des tclTHEN (cf dev/changements.txt) | herbelin |
