| Age | Commit message (Expand) | Author |
|---|
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-25 | Monomorphization (tactics) | ppedrot |
| 2012-11-08 | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot |
| 2012-10-01 | Added a new tactical infoH tac, that displays the names of hypothesis created... | courtieu |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-01 | Let's try to avoid generating induction principles for records (wish #2693) | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-03-30 | info_trivial, info_auto, info_eauto, and debug (trivial|auto) | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-06-10 | Moved allow_K to a unification flag | 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-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 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 |
