| Age | Commit message (Expand) | Author |
|---|
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-23 | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot |
| 2014-04-22 | Removing tactic compatibility layer from Elim. | Pierre-Marie Pédrot |
| 2014-04-22 | Simplifying interface of elimination tactics. They used dummy clausenvs, and | Pierre-Marie Pédrot |
| 2014-03-28 | Define Tactics.bring_hyps in the new monad. | Pierre-Marie Pédrot |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2014-03-03 | Fixing pervasive equalities. In particular, I removed the code that deleted | Pierre-Marie Pédrot |
| 2014-02-27 | Proofview.Notations: Now that (>>=) is free, use it for tclBIND. | Arnaud Spiwack |
| 2013-12-02 | Writing [cut] tactic using the new monad. | Pierre-Marie Pédrot |
| 2013-11-02 | Less use of the list-based interface for goal-bound tactics. | aspiwack |
| 2013-11-02 | Tachmach.New is now in Proofview.Goal.enter style. | aspiwack |
| 2013-11-02 | Removed spurious try/with in Proofview.Notation.(>>=) and (>>==). | 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 |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-10-06 | still some more dead code removal | letouzey |
| 2012-10-06 | remove Refiner.abstract_tactic and similar | letouzey |
| 2012-10-06 | Clean-up : removal of Proof_type.tactic_expr | letouzey |
| 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-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | Tacexpr as a mli-only, the few functions there are now in Tacops | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 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-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-03-14 | Cleaning/uniformizing the interface of tacticals.mli | herbelin |
| 2008-12-30 | - Fixed bugs and compatibilities issues in | herbelin |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2007-05-20 | - Propagation des evars non résolues vers les with_bindings; permet par exemple | herbelin |
| 2005-11-08 | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-03-01 | Déplacement définition intro_pattern_expr dans Genarg | herbelin |
| 2003-10-27 | Bug Double Inversion | herbelin |
| 2003-10-10 | Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion' | herbelin |
| 2003-06-13 | Utilisation de intro_pattern dans NewDestruct/NewInduction | herbelin |
| 2003-05-21 | Suppression définitive de lmatch et or_metanum dans tacinterp | herbelin |
| 2003-04-07 | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin |
| 2003-04-07 | code mort | herbelin |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-08-02 | Modules dans COQ\!\!\!\! | coq |
| 2002-05-29 | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin |
| 2002-02-15 | petits changements cosmetiques sur les tactiques | barras |
| 2002-02-07 | petit nettoyage de kernel/inductive | barras |
| 2002-02-01 | Ajout tactiques Rename et Pose; modifications pour Inversion | herbelin |
