| Commit message (Expand) | Author | Age |
* | Moving the decompose tactic out of the AST. | Pierre-Marie Pédrot | 2014-09-01 |
* | Removing spurious tclWITHHOLES. | Pierre-Marie Pédrot | 2014-08-27 |
* | Add an is_cofix tactic | Jason Gross | 2014-08-25 |
* | Removing a use of Goal.refine. | Pierre-Marie Pédrot | 2014-08-19 |
* | Slight simplification of naming of tactics in equality.ml (hopefully). | Hugo Herbelin | 2014-08-18 |
* | Reorganization of tactics: | Hugo Herbelin | 2014-08-18 |
* | Better structure for Ltac pretyping environments. | Pierre-Marie Pédrot | 2014-08-07 |
* | [uconstr]: use a closure instead of eager substitution. | Arnaud Spiwack | 2014-08-06 |
* | Experimentally adding an option for automatically erasing an | Hugo Herbelin | 2014-08-05 |
* | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi | 2014-08-05 |
* | The [refine] tactic now accepts [uconstr]. | Arnaud Spiwack | 2014-08-05 |
* | Add [guard] tactic. | Arnaud Spiwack | 2014-08-01 |
* | Add a tactic [swap i j] to swap the position of goals [i] and [j]. | Arnaud Spiwack | 2014-07-25 |
* | Adds a cycle tactic to reorder goals in a loop. | Arnaud Spiwack | 2014-07-25 |
* | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin | 2014-06-28 |
* | Oops, I fixed the .ml's | Matthieu Sozeau | 2014-06-23 |
* | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | 2014-06-18 |
* | Removing decompose record / sum from the tactic AST. | Pierre-Marie Pédrot | 2014-05-21 |
* | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot | 2014-05-12 |
* | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Removing the compatibility layer from Leminv. Also removed an undocumented | Pierre-Marie Pédrot | 2014-04-22 |
* | Closing bug #3260 | Julien Forest | 2014-04-14 |
* | Removing the Change_evar refiner rule. | Pierre-Marie Pédrot | 2014-03-31 |
* | Moving some tactic code to the new engine. | Pierre-Marie Pédrot | 2014-03-26 |
* | Proofview.Notations: Now that (>>=) is free, use it for tclBIND. | Arnaud Spiwack | 2014-02-27 |
* | Get rid of the enterl/glist API for Proofview.Goal. | Arnaud Spiwack | 2014-02-27 |
* | Exporting the full pretyper options in Goal.constr_of_raw. | Pierre-Marie Pédrot | 2014-01-10 |
* | Ensuring the right parsing of glob arguments, used by refine | Pierre-Marie Pédrot | 2013-12-01 |
* | Fixing ltac constr variable handling in refine. | Pierre-Marie Pédrot | 2013-11-30 |
* | Getting rid of casted_open_constr. It was only used by the | Pierre-Marie Pédrot | 2013-11-30 |
* | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot | 2013-11-27 |
* | Remove the Hiddentac module. | Arnaud Spiwack | 2013-11-25 |
* | Doc: solve the bad interaction between Declare Implicit Tactic and refine. | aspiwack | 2013-11-02 |
* | Refine: Tactics.New.refine does beta-reduction. | aspiwack | 2013-11-02 |
* | Adds a tactic give_up. | aspiwack | 2013-11-02 |
* | A tactic shelve_unifiable. | aspiwack | 2013-11-02 |
* | Adds a shelve tactic. | aspiwack | 2013-11-02 |
* | Refine does beta-reductions. | 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 |
* | Clean up a warning. | aspiwack | 2013-11-02 |
* | The tactic [admit] exits with the "unsafe" status. | aspiwack | 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-11-02 |
* | Moving side effects into evar_map. There was no reason to keep another | ppedrot | 2013-10-05 |
* | Vernac classification streamlined (handles VERNAC EXTEND) | gareuselesinge | 2013-08-08 |