| Age | Commit message (Expand) | Author |
|---|
| 2013-11-02 | A whole new implemenation of the refine tactic. | aspiwack |
| 2013-11-02 | Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations. | aspiwack |
| 2013-11-02 | Getting rid of Goal.here, and all the related exceptions and combinators. | aspiwack |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-25 | Monomorphization (tactics) | ppedrot |
| 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-04 | Forward-port fixes from 8.4 (15358, 15353, 15333). | msozeau |
| 2012-03-20 | Fix interface of resolve_typeclasses: onlyargs -> with_goals: | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-21 | Fix for bug #2350 was really too quick. Here is a version that works better. | herbelin |
| 2010-07-21 | Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic). | herbelin |
| 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-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-10-28 | Clarification in comments | glondu |
| 2009-10-27 | fixed czar bug with parametric inductives | corbinea |
| 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-06-06 | Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0 | herbelin |
| 2009-06-01 | ## Lines starting with '## ' will be removed from the log message. | msozeau |
| 2009-04-08 | - Fixing bug #2084 (unification not checking sort constraints), hoping | herbelin |
| 2009-03-14 | Cleaning/uniformizing the interface of tacticals.mli | herbelin |
| 2008-12-09 | About "apply in": | herbelin |
| 2008-11-04 | Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974) | herbelin |
| 2008-10-18 | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2007-05-19 | Backtrack sur l'effacement dans le contexte de but des lieurs | herbelin |
| 2007-05-18 | Wish #1582 (3eme) | herbelin |
| 2007-05-18 | Quelques essais autour du wish implicite au rapport de bug #1582 (2eme) | herbelin |
| 2007-05-18 | Quelques essais autour du wish implicite au rapport de bug #1582 | herbelin |
| 2006-11-10 | Correction d'un bug refine | herbelin |
| 2006-01-11 | Restructuration et simplification des fonctions d'affichage, de détypage | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-11-08 | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin |
| 2005-03-08 | Fix bug #931: leave dependent evars as such for refine | herbelin |
| 2004-12-09 | Restauration type casted_open_constr pour tactique refine car l'unification n... | herbelin |
| 2004-12-06 | Garder les cast semble décidément le meilleur moyen de rester synchrone ave... | herbelin |
| 2004-12-06 | Suppression des cast après avoir utiliser l'information de type (Tacinv envo... | herbelin |
| 2004-12-06 | Déplacement de la coercion vis à vis du but au niveau de Refine suite à ch... | herbelin |
| 2004-12-06 | Réparation bug #888 (les tactiques fix et cofix exigent autant de sous-buts ... | herbelin |
| 2004-09-12 | inclusion de meta_map dans evar_defs | barras |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-06-02 | bug #787 de Roland | barras |
| 2003-12-13 | Correction bug soumis par Yves | herbelin |
