| Age | Commit message (Expand) | Author |
|---|
| 2016-06-18 | Adding eintros to respect the e- prefix policy. | Hugo Herbelin |
| 2016-05-16 | Put the "exact" family of tactic in the monad. | Pierre-Marie Pédrot |
| 2016-05-16 | Put the "clear" tactic into the monad. | Pierre-Marie Pédrot |
| 2016-02-09 | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-21 | Fixing some problems with double induction. | Hugo Herbelin |
| 2016-01-20 | Code simplification in elim.ml. | Hugo Herbelin |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-14 | Moving is_quantified_hypothesis to new proof engine. | Hugo Herbelin |
| 2015-10-20 | Proofview.Goal.sigma returns an indexed evarmap. | Pierre-Marie Pédrot |
| 2015-10-20 | Boxing the Goal.enter primitive into a record type. | Pierre-Marie Pédrot |
| 2015-05-13 | Safer typing primitives. | Pierre-Marie Pédrot |
| 2015-02-02 | Removing dead code. | Pierre-Marie Pédrot |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey |
| 2014-09-06 | Renaming goal-entering functions. | Pierre-Marie Pédrot |
| 2014-08-18 | Reorganisation of intropattern code | Hugo Herbelin |
| 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 |
