| Age | Commit message (Expand) | Author |
|---|
| 2014-03-26 | Removing tactic compatibility layer in Equality. | Pierre-Marie Pédrot |
| 2014-03-26 | Removing Tacmach compatibility layer in Inv. | Pierre-Marie Pédrot |
| 2014-03-26 | Removing tactic compatibility layer from Inv. | Pierre-Marie Pédrot |
| 2014-03-19 | Using non-normalized goals in tactic interpretation. | Pierre-Marie Pédrot |
| 2014-03-07 | Useless tactic bindings in Tacticals. | Pierre-Marie Pédrot |
| 2014-02-27 | Proofview.Notations: Now that (>>=) is free, use it for tclBIND. | Arnaud Spiwack |
| 2013-11-04 | Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was sol... | aspiwack |
| 2013-11-04 | Fix ltac's progress tactical: requires progress in each goal. | aspiwack |
| 2013-11-04 | Fix the tactical ; [ … ] : the "incorrect number of goal" error was not cau... | aspiwack |
| 2013-11-02 | The repeat tactic now honors failure levels in ltac. | aspiwack |
| 2013-11-02 | Tacticals.New.tclWITHHOLES: clean up. | aspiwack |
| 2013-11-02 | Adds an experimental exactly_once tactical. | aspiwack |
| 2013-11-02 | Made Proofview.Goal.hyps a named_context. | aspiwack |
| 2013-11-02 | Adds a tactical once. | aspiwack |
| 2013-11-02 | Corrects the semantics of the "+" tactical. | aspiwack |
| 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 | More Proofview.Goal.enter. | aspiwack |
| 2013-11-02 | Added the tactical "tac1 + tac2". | aspiwack |
| 2013-11-02 | Various rewriting, mostly for speed purposes. | aspiwack |
| 2013-11-02 | Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by... | 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 | Bases tactics on an IO monad. | aspiwack |
| 2013-11-02 | Getting rid of Goal.here, and all the related exceptions and combinators. | aspiwack |
| 2013-11-02 | Uses Proofview.tclEXTEND more sparingly. | aspiwack |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-02-26 | kernel/declarations becomes a pure mli | letouzey |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 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 |
