| Commit message (Expand) | Author | Age |
* | Useless tactic bindings in Tacticals. | Pierre-Marie Pédrot | 2014-03-07 |
* | Proofview.Notations: Now that (>>=) is free, use it for tclBIND. | Arnaud Spiwack | 2014-02-27 |
* | 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-04 |
* | 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-11-02 |
* | Merging Context and Sign. | ppedrot | 2013-04-29 |
* | kernel/declarations becomes a pure mli | letouzey | 2013-02-26 |
* | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Monomorphization (tactics) | ppedrot | 2012-11-25 |
* | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot | 2012-11-08 |
* | Added a new tactical infoH tac, that displays the names of hypothesis created... | courtieu | 2012-10-01 |
* | 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-09-14 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
* | Let's try to avoid generating induction principles for records (wish #2693) | letouzey | 2012-06-01 |
* | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey | 2012-05-29 |
* | info_trivial, info_auto, info_eauto, and debug (trivial|auto) | letouzey | 2012-03-30 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | Moved allow_K to a unification flag | herbelin | 2011-06-10 |
* | A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds | letouzey | 2011-03-18 |
* | Rename rawterm.ml into glob_term.ml | glondu | 2010-12-23 |
* | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Applicative commutative cuts in Fixpoint guard condition | pboutill | 2010-05-18 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack | 2010-04-22 |
* | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin | 2009-11-08 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Use a lazy value for the message in FailError, so that it won't be | msozeau | 2009-06-11 |